Logic Verification of ANSI-C Code with Spin

(Title Originally issued as MCC: A Model Checker for Distributed Applications Written in C) Mcc consists of two parts: a model extractor and a verification engine. The system can be used to verify the logical properties of distributed software systems that are implemented in ANSI-standard C (KR88). Target applications include telephone switching software, distributed operating systems code, protocol implementations, concurrency control methods, and client-server applications. To verify an implementation, the user provides a property to be proven and a test harness. The test harness captures assumptions about the valid inputs and outputs of the application, and it contains the definition of a filter that can be used to set the desired level of abstraction. This paper discusses how a prototype for MCC's model extractor was implemented, and describes how we plan to extend it for the final version. The prototype version of MCC was used in the formal verification of two substantial software applications: a commercial checkpoint management system and the call processing code for a new telephone switch.