SAT-Based Software Certification
CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST
Pagination or Media Count:
This report formalizes a notion of witnesses as the basis of certifying the correctness of software. The first part of the report is concerned with witnesses for the satisfaction of linear temporal logic specifications by infinite state programs and shows how such witnesses may be constructed via predicate abstraction and validated by generating and proving verification conditions. In addition, the first part of the report proposes the use of theorem provers based on Boolean propositional satisfiability SAT and resolution proofs in validating these verification conditions. In addition to yielding extremely compact proofs, a SAT-based approach overcomes several limitations of conventional theorem provers when applied to the verification of programs written in real-life programming languages. The second part of this report formalizes a notion of witnesses of simulation conformance between infinite state programs and finite state machine specifications. The report also proves that computing a minimal simulation relation between two finite state machines is an NP-hard problem. Finally, the report presents algorithms to construct simulation witnesses of minimal size by solving pseudo-Boolean constraints. The authors experiments on several nontrivial benchmarks suggest that a SAT-based approach can yield extremely compact proofs -- in some cases by a factor of over 10exp 5 -- when compared to existing non-SAT-based theorem provers.
- Theoretical Mathematics
- Computer Programming and Software
- Computer Systems Management and Standards