Issue No. 06 - June (2004 vol. 30)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2004.22
Edmund M. Clarke , IEEE
<p><b>Abstract</b>—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 <b>C</b>ounter<b>E</b>xample <b>G</b>uided <b>A</b>bstraction <b>R</b>efinement (CEGAR) paradigm, our tool <scp>magic</scp> first extracts a finite model from C source code using predicate abstraction and theorem proving. Subsequently, weak simulation is checked via a reduction to Boolean satisfiability. <scp>magic</scp> has been interfaced with several publicly available theorem provers and SAT solvers. We report experimental results with procedures from the Linux kernel, the OpenSSL toolkit, and several industrial strength benchmarks.</p>
Software engineering, formal methods, verification.
Alex Groce, Edmund M. Clarke, Somesh Jha, Helmut Veith, Sagar Chaki, "Modular Verification of Software Components in C", IEEE Transactions on Software Engineering, vol. 30, no. , pp. 388-402, June 2004, doi:10.1109/TSE.2004.22