We will describe the design of a logic model checking
system for distributed software implementations written
in ANSI-standard C. The system, tentatively named MCC,
consists of a model extractor and a verification engine.
The model extractor derives labeled transition systems
from C source text, guided by a user-defined lookup
table that sets the required level of abstraction.
The verification engine (we use the Spin model checker)
performs the verification chores.
The verification models are instrumented in such a way
that property violations identified by Spin are reported
as step-by-step execution traces through the original C
source text of the application.
Last modified: Mon Apr 17 14:43:21 MET DST 2000