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.
People
|
Faculty |
|
|
Students |
|
|
Administration |
|
|
Past Members |
|
Selected Publications
| Decision Procedures – an Algorithmic Point of View Daniel Kroening and Ofer Strichman Springer. 2008. To appear |
| 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. |
