The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - June (2004 vol.30)
pp: 388-402
ABSTRACT
<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>
INDEX TERMS
Software engineering, formal methods, verification.
CITATION
Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith, "Modular Verification of Software Components in C", IEEE Transactions on Software Engineering, vol.30, no. 6, pp. 388-402, June 2004, doi:10.1109/TSE.2004.22
17 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool