Predicate abstraction is a major method for verification of software. However, the generation of the abstract Boolean program from the set of predicates and the original program suffers from an exponential number of theorem prover calls as well as from soundness issues. This paper presents a novel technique that uses an efficient SAT solver for generating the abstract transition relation of ANSI-C programs. The SAT-based approach computes a more precise and safe abstraction compared to existing predicate abstraction techniques.
Published in the Proceedings of the Model Checking for
Dependable Software-Intensive Systems Workshop held as part of
the International Conference on Dependable Systems and Networks 2003, journal version 35 pages.
PostScript(gz) /
PDF
© 2003 Natasha Sharygina.