Loading...
Please wait, while we are loading the content...
Similar Documents
Modular Verification of Software Components in C (2004)
| Content Provider | CiteSeerX |
|---|---|
| Author | Chaki, Sagar Clarke, Edmund Groce, Alex Jha, Somesh Veith, Helmut |
| Description | 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. |
| File Format | |
| Journal | IEEE Transactions on Software Engineering |
| Language | English |
| Publisher Date | 2004-01-01 |
| Access Restriction | Open |
| Subject Keyword | Source Code Software Component Predicate Abstraction Boolean Satisfiability Large Software System Automatic Verification Tool Magic Theorem Proving Abstraction Refinement Weak Simulation Finite State Machine Specification Finite Model Manageable Complexity New Methodology Software Design Modular Verification |
| Content Type | Text |
| Resource Type | Article |
