Boost the Impact of Continuous Formal Verification in Industry
Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro

TL;DR
This paper proposes integrating software model checking into DevOps workflows by automating continuous formal verification guided by regression tests, aiming to enhance scalability and practical adoption in industry.
Contribution
It introduces a novel approach to embed formal verification into continuous integration, focusing on incremental verification guided by regression tests within developer workflows.
Findings
Improves scalability of formal verification in industry settings.
Facilitates integration of formal methods into daily software development.
Enhances verification efficiency through regression test-guided processes.
Abstract
Software model checking has experienced significant progress in the last two decades, however, one of its major bottlenecks for practical applications remains its scalability and adaptability. Here, we describe an approach to integrate software model checking techniques into the DevOps culture by exploiting practices such as continuous integration and regression tests. In particular, our proposed approach looks at the modifications to the software system since its last verification, and submits them to a continuous formal verification process, guided by a set of regression test cases. Our vision is to focus on the developer in order to integrate formal verification techniques into the developer workflow by using their main software development methodologies and tools.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Formal Methods in Verification · Software Reliability and Analysis Research
