MCP is an explicit-state software model checker that supports the entire C++ programming language. In this demonstration, we will describe its architecture and present some initial results.

Introduction

The MCP (Model checker for C Plus plus) model checker was constructed specifically to allow programs written in C or C++ to be model-checked directly without requiring prior translation or model extraction.It builds upon the LLVM compiler infrastructure, thereby avoiding the requirement to directly recognise the (extremely complex) C++ language at source-level. This approach has allowed us to support the entire C++ language, including templates. The C language is handled fully, not just as an improper subset of C++. NASA has been involved with research on software model checking for some time. Our group at NASA Ames developed Java Pathfinder (JPF) , a publicly available software model checker for the Java language. Our colleagues at JPL developed the well-known SPIN model checker. Experience from the JPF project has demonstrated the utility of software model checking (i.e. model checking that acts directly on a program, rather than on a model that has been manually extracted from it). However, current fight software is mostly implemented in C, not Java, and in future it seems increasingly likely that C++ will become the platform of choice. The MCP model checker was developed to fill the requirement for an explicit-state software model checker, in the style of JPF, that fully supports the C++ language.

MCP ARCHITECTURE

MCP is, in efect, a heavily modifed, extended interpreter for LLVM bytecode that supports threads, state abstraction and a variety of search strategies. No attempt is made to extract a model from the code; rather, the code is executed directly, trying all possible interleavings, with the intention of triggering otherwise-deeply-hidden assertions. MCP's bytecode interpreter has the responsibility of executing LLVM instructions. All memory access is mediated through a versioning memory management subsystem that allows the state to be checkpointed at any time, and for the current state to be rolled effciently to any other saved state. Threading is implemented in such a way as to allow user-supplied threading subsystems to be loaded, thereby enabling the emulation of the majority of operating system threading models. A state queue maintains the list of states that have yet to be evaluated; manipulating the order in which states are added and removed from this queue allows a variety of search strategies to be implemented.

Last modified: Aug. 22, 2008 by Allen Dutra.