Modular verification of software components in C

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

Research output: Contribution to journalArticlepeer-review

168 Scopus citations

Abstract

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 CounterExample Guided Abstraction Refinement (CEGAR) paradigm, our tool MAGIC 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. MAGIC 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.

Original languageEnglish (US)
Pages (from-to)388-402
Number of pages15
JournalIEEE Transactions on Software Engineering
Volume30
Issue number6
DOIs
StatePublished - Jun 2004
Externally publishedYes

Keywords

  • Formal methods
  • Software engineering
  • Verification

ASJC Scopus subject areas

  • Software

Fingerprint

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

Cite this