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.

Selected Publications

View All

• Decision Procedures – an Algorithmic Point of View

  Daniel Kroening and Ofer Strichman

  Springer. 2008.

  To appear

  Details about Decision Procedures – an Algorithmic Point of View | BibTeX data for Decision Procedures – an Algorithmic Point of View

• 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.

  Details about A Survey of Automated Techniques for Formal Software Verification | BibTeX data for A Survey of Automated Techniques for Formal Software Verification | DOI (10.1109/TCAD.2008.923410) | Link to A Survey of Automated Techniques for Formal Software Verification