Journal article

A survey of automated techniques for formal software verification

Abstract:: The quality and the correctness of software are often the greatest concern in electronic systems. Formal verification tools can provide a guarantee that a design is free of specific flaws. This paper surveys algorithms that perform automatic static analysis of software to detect programming errors or prove their absence. The three techniques considered are static analysis with abstract domains, model checking, and bounded model checking. A short tutorial on these techniques is provided, highlighting their differences when applied to practical problems. This paper also surveys tools implementing these techniques and describes their merits and shortcomings.

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.
Cite

Cite this record

APA Style

D'Silva, V., Kroening, D., & Weissenbacher, G. (2008). A survey of automated techniques for formal software verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(7), 1165–1178.

MLA Style

D'Silva, V., et al. “A Survey of Automated Techniques for Formal Software Verification.” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 27, no. 7, Institute of Electrical and Electronics Engineers, 2008, pp. 1165–78.

Chicago Style

D'Silva, V, D Kroening, and G Weissenbacher. 2008. “A Survey of Automated Techniques for Formal Software Verification.” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 27 (7): 1165–78.
Share
Print

Access Document

Files:: tcad-sw-2008.pdf

(Preview, Accepted manuscript, pdf, 905.5KB, Terms of use)

Publisher copy:: 10.1109/TCAD.2008.923410

Authors

+ D'Silva, V More by this author

Role:: Author

+ Kroening, D More by this author

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

+ Weissenbacher, G More by this author

Role:: Author

Publisher:: Institute of Electrical and Electronics Engineers
Journal:: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems More from this journal
Volume:: 27
Issue:: 7
Pages:: 1165-1178
Publication date:: 2008-07-01
DOI:: 10.1109/TCAD.2008.923410
ISSN:: 0278-0070

Keywords:: SBTMR
Pubs id:: pubs:327161
UUID:: uuid:78a5fb01-da63-4b6f-a894-a723e4489273
Local pid:: pubs:327161
Source identifiers:: 327161
Deposit date:: 2017-01-28

Terms of use

Copyright holder:: Institute of Electrical and Electronics Engineers
Copyright date:: 2008
Notes:: © 2008 IEEE. This is the accepted manuscript version of the article. The final version is available online from IEEE at: r 10.1109/TCAD.2008.923410

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