Modular verification of software components in C

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

Full description

Saved in:
Bibliographic Details
Main Authors: Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.
Format: Conference Proceeding
Language:English
Subjects:
Automata
Kernel
Linux
Programming
Protocols
Software design
Software engineering
Software systems
Unified modeling language
Visualization
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0270-5257
1558-1225
DOI:10.1109/ICSE.2003.1201217