Skip to main content

A Survey of Automated Techniques for Formal Software Verification

Vijay D'Silva‚ Daniel Kroening and Georg Weissenbacher

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

Journal
IEEE Transactions on Computer−Aided Design of Integrated Circuits and Systems (TCAD)
Month
July
Number
7
Pages
1165−1178
Publisher
IEEE
Volume
27
Year
2008