Model driven code checking

Gerard J. Holzmann, Rajeev Joshi, Alex Groce

Research output: Contribution to journalArticlepeer-review

27 Scopus citations


Model checkers were originally developed to support the formal verification of high-level design models of distributed system designs. Over the years, they have become unmatched in precision and performance in this domain. Research in model checking has meanwhile moved towards methods that allow us to reason also about implementation level artifacts (e.g., software code) directly, instead of hand-crafted representations of those artifacts. This does not mean that there is no longer a place for the use of high-level models, but it does mean that such models are used in a different way today. In the approach that we describe here, high-level models are used to represent the environment for which the code is to be verified, but not the application itself. The code of the application is now executed as is by the model checker, while using powerful forms of abstraction on-the-fly to build the abstract state space that guides the verification process. This model-driven code checking method allows us to verify implementation level code efficiently for high-level safety and liveness properties. In this paper, we give an overview of the methodology that supports this new paradigm of code verification.

Original languageEnglish (US)
Pages (from-to)283-297
Number of pages15
JournalAutomated Software Engineering
Issue number3-4 SPEC. ISS.
StatePublished - Dec 2008
Externally publishedYes


  • Embedded C code
  • Logic model checking
  • Software verification
  • Spin model checker

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Model driven code checking'. Together they form a unique fingerprint.

Cite this