Logic Verification of ANSI-C Code with SPIN

13 years 11 months ago
Logic Verification of ANSI-C Code with SPIN
We describe a tool, called AX, that can be used in combination with the model checker SPIN to efficiently verify logical properties of distributed software systems implemented in ANSI-standard C [18]. AX, short for Automaton eXtractor, can extract verification models from C code at a user level of abstraction. Target applications include telephone switching software, distributed operating systems code, protocol implementations, concurrency control methods, and client-server applications. This paper discusses how AX is currently implemented, and how we plan to extend it. The tool 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.
Gerard J. Holzmann
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where SPIN
Authors Gerard J. Holzmann
Comments (0)