Software Model Checking
Manual inspection of complex software is error-prone and costly, and tool support is in dire need. Model Checking is an
automated technique, and tools that implement it check the behaviour of a program for all vectors of inputs. Numerous
tools to hunt down functional design flaws in hardware designs have been available commercially for a number years, mainly
because of the enormous cost of hardware bugs. The use of such tools
is widespread, and there is a broad range of vendors. In contrast, the market for formal tools that address the need for quality software is still in its infancy.
The promise of automated bug finding in complex software is not new. The Verifying Compiler was identified as a research goal already in the 70s, and recently re-stated as a `Grand Challenge' by Tony Hoare for computing research. While the problem in general is not yet solved, tools that specialise in very specific aspects of the problem have been able to show impact.
Decision Procedures – an Algorithmic Point of View
Daniel Kroening and Ofer Strichman
A Survey of Automated Techniques for Formal Software Verification
Vijay D'Silva‚ Daniel Kroening and Georg Weissenbacher
In IEEE Transactions on Computer−Aided Design of Integrated Circuits and Systems (TCAD). Vol. 27. No. 7. Pages 1165−1178. July, 2008.