RECORD
Model Checking Software Programs with First Order Logic Specifications using AIG Solvers
Software Engineering · Submitted 24 Sep 2014
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim 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.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
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.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | 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. | background 1.00 | 0.04 | 0.04 | asserted 1.00 |
| s1 | They force bounds on variable ranges and execution time and translate the program and its specifications into a Boolean formula. | background 0.94 | 0.07 | 0.03 | asserted 1.00 |
| s2 | They are limited to programs of relatively low complexity for the following reasons. | background 0.77 | 0.08 | 0.03 | asserted 1.00 |
| s3 | (1) A small increase in the bounds can cause a large increase in the size of the translated formula. | background 0.73 | 0.14 | 0.02 | asserted 0.98 |
| s4 | (2) Boolean satisfiability solvers are restricted to using optimizations that apply at the level of the formula. | background 0.72 | 0.06 | 0.02 | asserted 1.00 |
| s5 | Finally, (3) the Boolean formulae often need to be regenerated with higher bounds to ensure the correctness of the translation. | background 0.76 | 0.11 | 0.02 | asserted 0.85 |
| s6 | 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. | contribution 0.92 | 0.89 | 0.48 | asserted 1.00 |
| s7 | (1) Sequential circuits are much more succinct than Boolean formulae with no memory elements and preserve the high-level structure of the program. | contribution 0.66 | 0.35 | 0.16 | asserted 1.00 |
| s8 | (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. | contribution 0.77 | 0.27 | 0.15 | asserted 0.99 |
| s9 | 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. | method 0.89 | 0.91 | 0.28 | asserted 1.00 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
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.
Human review
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.