Modular verification of software components in C
- 1 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 1579 (02705257) , 385-395
- https://doi.org/10.1109/icse.2003.1201217
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 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.Keywords
This publication has 16 references indexed in Scilit:
- A system and language for building system-specific, static analysesPublished by Association for Computing Machinery (ACM) ,2002
- ICS: Integrated Canonizer and Solver?Published by Springer Nature ,2001
- Automatic predicate abstraction of C programsPublished by Association for Computing Machinery (ACM) ,2001
- Boolean and Cartesian Abstraction for Model Checking C ProgramsPublished by Springer Nature ,2001
- Counterexample-Guided Abstraction RefinementPublished by Springer Nature ,2000
- Symbolic Model Checking without BDDsPublished by Springer Nature ,1999
- Experience with Predicate AbstractionPublished by Springer Nature ,1999
- Model checking and abstractionACM Transactions on Programming Languages and Systems, 1994
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- Linear-time algorithms for testing the satisfiability of propositional horn formulaeThe Journal of Logic Programming, 1984