Loading...
Please wait, while we are loading the content...
Similar Documents
Abstraction and assume-guarantee reasoning for automated software verification
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Giannakopoulou, D. Chaki, S. Clarke, E. Pasareanu, C. S. |
| Copyright Year | 2004 |
| Description | Compositional verification and abstraction are the key techniques to address the state explosion problem associated with model checking of concurrent software. A promising compositional approach is to prove properties of a system by checking properties of its components in an assume-guarantee style. This article proposes a framework for performing abstraction and assume-guarantee reasoning of concurrent C code in an incremental and fully automated fashion. The framework uses predicate abstraction to extract and refine finite state models of software and it uses an automata learning algorithm to incrementally construct assumptions for the compositional verification of the abstract models. The framework can be instantiated with different assume-guarantee rules. We have implemented our approach in the COMFORT reasoning framework and we show how COMFORT out-performs several previous software model checking approaches when checking safety properties of non-trivial concurrent programs. |
| File Size | 1083265 |
| Page Count | 18 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20050185529 |
| Archival Resource Key | ark:/13960/t4dn93m2v |
| Language | English |
| Publisher Date | 2004-10-01 |
| Access Restriction | Open |
| Subject Keyword | Computer Programming And Software Algorithms Automata Theory Machine Learning C Programming Language Models Program Verification Computers Computer Programs Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |
