|
|||||
|
|
Predicate Abstraction of ANSI-C Programs Using SAT |
|
| Authors: | Edmund Clarke Daniel Kroening Natasha Sharygina Karen Yorav |
| Affiliation: | 1. Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 2. Computer Systems Institute, Swiss Institute of Technology, Zurich, Switzerland 3. Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA 4. IBM, Haifa, Israel |
| Abstract: | Predicate abstraction is a major method for verification of software. However, the generation of the abstract Boolean program from the set of predicates and the original program suffers from an exponential number of theorem prover calls as well as from soundness issues. This paper presents a novel technique that uses an efficient SAT solver for generating the abstract transition relations of ANSI-C programs. The SAT-based approach computes a more precise and safe abstraction compared to existing predicate abstraction techniques. |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ | |