Modular verification of software components in C

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

doi:10.1109/TSE.2004.22

Modular verification of software components in C

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

Research output: Contribution to journal › Article › peer-review

180 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 language	English (US)
Pages (from-to)	388-402
Number of pages	15
Journal	IEEE Transactions on Software Engineering
Volume	30
Issue number	6
DOIs	https://doi.org/10.1109/TSE.2004.22
State	Published - Jun 2004
Externally published	Yes

Keywords

Formal methods
Software engineering
Verification

ASJC Scopus subject areas

Software

Access to Document

10.1109/TSE.2004.22

Cite this

@article{02bf3a9669c0482cb331a024488ad247,

title = "Modular verification of software components in C",

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.",

keywords = "Formal methods, Software engineering, Verification",

author = "Sagar Chaki and Clarke, {Edmund M.} and Alex Groce and Somesh Jha and Helmut Veith",

note = "Funding Information: Several people have contributed, and continue to contribute, critically to the progress of the MAGIC project. In particular, the authors would like to thank Jo{\"e}l Ouaknine, Nishant Sinha, Natasha Sharygina, Ofer Strichman, and Karen Yorav for making MAGIC happen. This research was supported by the ONR under Grant No. N00014-01-1-0796, by the US National Science Foundation (NSF) under Grant No. CCR-9803774, CCR-0121547, and CCR-0098072, by the ARO under Grant No. DAAD 19-01-1-0485, the Austrian Science Fund Project NZ29-INF, the EU Research and Training Network GAMES, and graduate student fellowships from Microsoft and the NSF. Any opinions, findings and conclusions, or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF or the US Government.",

year = "2004",

month = jun,

doi = "10.1109/TSE.2004.22",

language = "English (US)",

volume = "30",

pages = "388--402",

journal = "IEEE Transactions on Software Engineering",

issn = "0098-5589",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

number = "6",

}

TY - JOUR

T1 - Modular verification of software components in C

AU - Chaki, Sagar

AU - Clarke, Edmund M.

AU - Groce, Alex

AU - Jha, Somesh

AU - Veith, Helmut

N1 - Funding Information: Several people have contributed, and continue to contribute, critically to the progress of the MAGIC project. In particular, the authors would like to thank Joël Ouaknine, Nishant Sinha, Natasha Sharygina, Ofer Strichman, and Karen Yorav for making MAGIC happen. This research was supported by the ONR under Grant No. N00014-01-1-0796, by the US National Science Foundation (NSF) under Grant No. CCR-9803774, CCR-0121547, and CCR-0098072, by the ARO under Grant No. DAAD 19-01-1-0485, the Austrian Science Fund Project NZ29-INF, the EU Research and Training Network GAMES, and graduate student fellowships from Microsoft and the NSF. Any opinions, findings and conclusions, or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF or the US Government.

PY - 2004/6

Y1 - 2004/6

N2 - 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.

AB - 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.

KW - Formal methods

KW - Software engineering

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=3042666526&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=3042666526&partnerID=8YFLogxK

U2 - 10.1109/TSE.2004.22

DO - 10.1109/TSE.2004.22

M3 - Article

AN - SCOPUS:3042666526

SN - 0098-5589

VL - 30

SP - 388

EP - 402

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

IS - 6

ER -

Modular verification of software components in C

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this