Journal article icon

Journal article

Predicate Abstraction of ANSI-C Programs Using SAT

Abstract:
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 relations of ANSI-C programs. The SAT-based approach computes a more precise and safe abstraction compared to existing predicate abstraction techniques.
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Accepted Manuscript

Actions


Access Document


Files:
Publisher copy:
10.1023/B:FORM.0000040025.89719.f3

Authors


More by this author
Institution:
Carnegie Mellon University
Department:
Computer Science Department
Role:
Author
More by this author
Institution:
University of Oxford
Oxford college:
Magdalen College
Department:
Mathematical,Physical & Life Sciences Division - Computing Laboratory
Role:
Author
More by this author
Institution:
University of Lugano
Department:
Informatics Department
Role:
Author
More by this author
Institution:
IBM Haifa, Israel
Role:
Author
Publisher:
Kluwer Academic Publishers (Springer) Publisher's website
Journal:
Formal Methods in System Design Journal website
Volume:
25
Issue:
2-3
Pages:
105-127
Publication date:
2004-09-05
DOI:
EISSN:
1572-8102
ISSN:
0925-9856
URN:
uuid:76f11878-15a1-4027-ba03-03be6c19bd7c
Local pid:
ora:1711

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP