SAT-Based Software Certification
Sagar
Chaki,
Proceedings of the 12th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS), LNCS
3920, page 151-166, March 25-April 2, 2006
Abstract:
We formalize a notion of witnesses for satisfaction of linear temporal
logic specifications by infinite state programs. We show how such
witnesses may be constructed via predicate abstraction, and validated
by generating verification conditions and proving them. We propose the
use of SAT-based theorem provers and resolution proofs in proving
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. We also formalize
a notion of witnesses of simulation conformance between infinite state
programs and finite state machine specifications. We present
algorithms to construct simulation witnesses of minimal size by
solving pseudo-Boolean constraints. We present experimental results on
several non-trivial benchmarks which suggest that a SAT-based approach
can yield extremely compact proofs, in some cases by a factor of over
105, when compared to existing non-SAT-based theorem
provers.
PDF /
Online
© Springer