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.
