A Survey of Automated Techniques for Formal Software Verification

The quality and the correctness of software is 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 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. The paper also surveys the tools that are available implementing these techniques, and describes their merits and shortcomings.

• Type: Journal
• Year: 2008
• Where: TCAD
• Authors: Vijay D'Silva, Daniel Kroening, Georg Weissenbacher
• Keywords: Formal Verification Tools, Greatest Concern, Specific Flaws, TCAD 2008