Model Checking Software Programs with First Order Logic Specifications using AIG Solvers
This addresses scalability challenges in software verification for developers and researchers, though it is incremental as it builds on existing sequential circuit frameworks.
The paper tackles the problem of static verification of software programs using Boolean formula satisfiability solvers, which are limited by scalability issues with complex programs, and presents a method using sequential circuits that are more succinct and enable powerful automated analysis techniques, resulting in improved scalability for program validation.
Static verification techniques leverage Boolean formula satisfiability solvers such as SAT and SMT solvers that operate on conjunctive normal form and first order logic formulae, respectively, to validate programs. They force bounds on variable ranges and execution time and translate the program and its specifications into a Boolean formula. They are limited to programs of relatively low complexity for the following reasons. (1) A small increase in the bounds can cause a large increase in the size of the translated formula. (2) Boolean satisfiability solvers are restricted to using optimizations that apply at the level of the formula. Finally, (3) the Boolean formulae often need to be regenerated with higher bounds to ensure the correctness of the translation. We present a method that uses sequential circuits, Boolean formulae with memory elements and hierarchical structure, and sequential circuit synthesis and verification frameworks to validate programs. (1) Sequential circuits are much more succinct than Boolean formulae with no memory elements and preserve the high-level structure of the program. (2) Encoding the problem as a sequential circuit enables the use of a number of powerful automated analysis techniques that have no counterparts for other Boolean formulae. Our method takes an imperative program with a first order logic specification consisting of a precondition and a postcondition pair, and a bound on the program variable ranges, and produces a sequential circuit with a designated output that is true when the program violates the specification.