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
- Files:
-
-
(Accepted manuscript, pdf, 168.4KB)
-
- Publisher copy:
- 10.1023/B:FORM.0000040025.89719.f3
Authors
Bibliographic Details
- 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-01
- DOI:
- EISSN:
-
1572-8102
- ISSN:
-
0925-9856
Item Description
- Language:
- English
- Keywords:
- Subjects:
- UUID:
-
uuid:76f11878-15a1-4027-ba03-03be6c19bd7c
- Local pid:
- ora:1711
- Deposit date:
- 2008-03-14
Related Items
Terms of use
- Copyright holder:
- Kluwer Academic Publishers
- Copyright date:
- 2004
If you are the owner of this record, you can report an update to it here: Report update to this record