Combining predicate and numeric abstraction for software model checking |
| |
Authors: | Arie Gurfinkel Sagar Chaki |
| |
Affiliation: | 1. Software Engineering Institute, Carnegie Mellon University, Pittsburgh, USA
|
| |
Abstract: | Predicate (PA) and numeric (NA) abstractions are the two principal techniques for software analysis. In this paper, we develop
an approach to couple the two techniques tightly into a unified framework via a single abstract domain called NumPredDom. In particular, we develop and evaluate four data structures that implement NumPredDom but differ in their expressivity and internal representation and algorithms. All our data structures combine BDDs (for efficient
propositional reasoning) with data structures for representing numerical constraints. Our technique is distinguished by its
support for complex transfer functions that allow two-way interaction between predicate and numeric information during state
transformation. We have implemented a general framework for reachability analysis of C programs on top of our four data structures.
Our experiments on non-trivial examples show that our proposed combination of PA and NA is more powerful and more efficient
than either technique alone. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |