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

Email

Email this record

Send the bibliographic details of this record to your email address.

Your Email
Please enter the email address that the record information will be sent to.

-
Your message (optional)
Please add any additional information to be included within the email.
Share
Cite

Cite this record

APA Style

Clarke, E., Kroening, D., Sharygina, N., & Yorav, K. (2004). Predicate Abstraction of ANSI-C Programs Using SAT. Formal Methods in System Design, 25(2-3), 105–127.

MLA Style

Clarke, E, et al. “Predicate Abstraction of ANSI-C Programs Using SAT.” Formal Methods in System Design, Accepted Manuscript, vol. 25, nos. 2-3, 2004, pp. 105–27.

Chicago Style

Clarke, E, D Kroening, N Sharygina, and K Yorav. 2004. “Predicate Abstraction of ANSI-C Programs Using SAT.” Formal Methods in System Design 25 (2-3): 105–27.
Print

Access Document

Files:: Predicate abstraction of ANSI-C programs using SAT

(Accepted manuscript, bin, 168.4KB, Terms of use)

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

Authors

+ Clarke, E More by this author

Institution:: Carnegie Mellon University
Department:: Computer Science Department
Role:: Author

+ Kroening, D More by this author

Institution:: University of Oxford
Division:: MPLS
Department:: Computer Science
Oxford college:: Magdalen College
Role:: Author

+ Sharygina, N More by this author

Institution:: University of Lugano
Department:: Informatics Department
Role:: Author

+ Yorav, K More by this author

Institution:: IBM Haifa, Israel
Role:: Author

Publisher:: Kluwer Academic Publishers (Springer)
Journal:: Formal Methods in System Design More from this journal
Volume:: 25
Issue:: 2-3
Pages:: 105-127
Publication date:: 2004-09-01
Edition:: Accepted Manuscript
DOI:: 10.1023/B:FORM.0000040025.89719.f3
EISSN:: 1572-8102
ISSN:: 0925-9856

Language:: English
Keywords:: ANSI-C programs

predicate abstraction

SAT solver
Subjects:: Theory and automated verification

Software engineering

Applications and algorithms

Program development and tools
UUID:: uuid:76f11878-15a1-4027-ba03-03be6c19bd7c
Local pid:: ora:1711
Deposit date:: 2008-03-14
ARK identifier:: ark:/29072/ora_76f1187815a14027ba0303be6c19bd7c

Terms of use

Copyright holder:: Kluwer Academic Publishers
Copyright date:: 2004

Licence:: Terms and Conditions of Use for Oxford University Research Archive

Views and Downloads

About 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