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

Actions


Access Document


Authors


More by this author
Department:
Oxford, MPLS, Computer Science
Sharygina, N More by this author
Publisher:
Springer Publisher's website
Journal:
Formal Methods in System Design Journal website
Volume:
25
Issue:
2/3
Pages:
105-127
Publication date:
2004-09-01
DOI:
ISSN:
0925-9856
Pubs id:
pubs:327198
URN:
uri:b3c4bf2a-8f09-4004-a4c7-72c7485ad0b5
UUID:
uuid:b3c4bf2a-8f09-4004-a4c7-72c7485ad0b5
Local pid:
pubs:327198
Keywords:

Terms of use


Metrics



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

TO TOP