Case Studies

We believe that is important to try to model check properties of real software systems for a number of reasons.

  • Validation of our approach to abstraction-based model checking
  • Evaluation of the relative performance of different automated verification tools
  • Uncover specific cases where verification technology is particularly appropriate or inappropriate (and guide the development of new technology)

Our initial case studies have been done for programs (and parts of programs) written in Ada. We have a toolset that automates much of the work involved in translating Ada source code to finite-state models; the rest is done by hand for these studies. We make an effort to include all of intermediate artifacts constructed during this translation process, the property specifications, and data on the results of running the model checks in reporting on the case studies.

The original Ada case studies are here

Case studies of Java software are slowly accumulating