Computer Science Department
School of Computer Science, Carnegie Mellon University
Predicate Abstraction of ANSI-C Programs using SAT
Edmund Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
September 2003
CMU-CS-03-186.ps
CMU-CS-03-186.pdf
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.
25 pages
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu
School of Computer Science homepage