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