Modular Verification of Software Components in C
We present a new methodology for automatic verification of C programs
against finite state machine specifications. Our approach is
compositional, naturally enabling us to decompose the verification of large
software systems into subproblems of manageable complexity. The decomposition
reflects the modularity in the software design. We use weak simulation as the
notion of conformance between the program and its specification.
Following the abstract-verify-refine paradigm, our tool $\tool$ 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. $\tool$ is able to interface with several publicly
available theorem provers and SAT solvers. We report experimental results
with procedures from the Linux kernel and the OpenSSL toolkit.
Last modified: Fri Apr 11 14:46:15 CDT 2003