Modular verification of software components in C

Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith

Research output: Contribution to journalConference articlepeer-review

194 Scopus citations


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 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. We report experimental results with procedures from the Linux kernel and the OpenSSL toolkit.

Original languageEnglish (US)
Pages (from-to)385-395
Number of pages11
JournalProceedings - International Conference on Software Engineering
StatePublished - 2003
Externally publishedYes
Event25th International Conference on Software Engineering - Portland, OR, United States
Duration: May 3 2003May 10 2003

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Modular verification of software components in C'. Together they form a unique fingerprint.

Cite this