Modular verification of software components in C

9 August 2004

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering

Vol. 30 (6) , 388-402
https://doi.org/10.1109/tse.2004.22

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

This publication has 30 references indexed in Scilit:

A system and language for building system-specific, static analyses
Published by Association for Computing Machinery (ACM) ,2002
Boolean and Cartesian Abstraction for Model Checking C Programs
Published by Springer Nature ,2001
COM revisited
ACM SIGSOFT Software Engineering Notes, 2000
Automating first-order relational logic
ACM SIGSOFT Software Engineering Notes, 2000
Model checking JAVA programs using JAVA PathFinder
International Journal on Software Tools for Technology Transfer, 2000
Exploring the design of an intentional naming scheme with an automatic constraint analyzer
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2000
Model checking and abstraction
ACM Transactions on Programming Languages and Systems, 1994
On-line algorithms for polynomially solvable satisfiability problems
The Journal of Logic Programming, 1991
Automatic verification of finite-state concurrent systems using temporal logic specifications
ACM Transactions on Programming Languages and Systems, 1986
Linear-time algorithms for testing the satisfiability of propositional horn formulae
The Journal of Logic Programming, 1984