Extending model checking with dynamic analysis

Alex Groce, Rajeev Joshi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations


In model-driven verification a model checker executes a program by embedding it within a test harness, thus admitting program verification without the need to translate the program, which runs as native code. Model checking techniques in which code is actually executed have recently gained popularity due to their ability to handle the full semantics of actual implementation languages and to support verification of rich properties. In this paper, we show that combination with dynamic analysis can, with relatively low overhead, considerably extend the capabilities of this style of model checking. In particular, we show how to use the CIL framework to instrument code in order to allow the SPIN model checker, when verifying C programs, to check additional properties, simulate system resets, and use local coverage information to guide the model checking search. An additional benefit of our approach is that instrumentations developed for model checking may be used without modification in testing or monitoring code. We are motivated by experience in applying model-driven verification to JPL-developed flight software modules, from which we take our example applications. We believe this is the first investigation in which an independent instrumentation for dynamic analysis has been integrated with model checking.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 9th International Conference, VMCAI 2008, Proceedings
Number of pages15
StatePublished - 2008
Externally publishedYes
Event9th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2008 - San Francisco, CA, United States
Duration: Jan 7 2008Jan 9 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4905 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference9th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2008
Country/TerritoryUnited States
CitySan Francisco, CA

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Extending model checking with dynamic analysis'. Together they form a unique fingerprint.

Cite this