Program verification methodologies have come a long way, from handling simple textbook examples, useful only in classrooms, to automatic verification of industrial-strength programs with 50,000 lines of C code. However, even today’s tools are not easily usable by end programmers who lack sufficient grounding in mathematical logic and formal methods. This paper reports on work that could go a long way toward closing this gap; it is essential reading for students and researchers working in the area of software verification.

Based on the counterexample guided abstraction refinement paradigm for software development, the authors describe how their tool, modular analysis of programs in C (MAGIC), first extracts models (labeled transition systems) from the control flow graph of C programs, using predicate abstractions and theorem proving. MAGIC then uses weak simulation to check if the extracted implementation model conforms to the required specifications, also given as a labeled transition system (not as natural as temporal logic specifications). The main advantage of MAGIC is that most of the steps are automated. Its open design allows easy integration of any new or improved tools for theorem proving and satisfiability checking.

The paper concludes with some interesting analyses of how MAGIC performed on a few real-world examples, including the server-side handshake of the open secure sockets layer (SSL) implementation, and some interesting directions for future research. The paper is very lucidly written, with a brief review of related approaches and tools, both for Java and C, and with a wealth of useful references. It will be an excellent starting point for anyone interested in recent advances in software verification.