Modular Verification of Software Components in C
The authors present a new methodology for automatic verification of C programs against finite state machine specifications. The approach is compositional, naturally enabling one to decompose the verification of large software systems into subproblems of manageable complexity. The decomposition reflects the modularity in the software design. They use weak simulation as the notion of conformance between the program and its specification. Following the abstract verify-refine paradigm, the tool MAGIC first extracts a finite model from C source code using predicate abstraction and theorem proving. Subsequently, simulation is checked via a reduction to Boolean satisfiability. MAGIC is able to interface with several publicly available theorem provers and SAT solvers.