Software Engineering Institute

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 this 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 author's experiments on several nontrivial benchmarks suggest that a SAT-based approach can yield extremely compact proofs.