A Survey of Automated Techniques for Formal Software Verification

Publication Type:

Journal Article


A Survey of Automated Techniques for Formal Software Verification, IEEE (2008)




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