Approximation Refinement for Interpolation−Based Model Checking
Vijay D'Silva‚ Mitra Purandare and Daniel Kroening
Abstract
Model checking using Craig interpolants provides an effective method for computing an over-approximation of the set of reachable states using a SAT solver. This method requires proofs of unsatisfiability from the SAT solver to progress. If an over-approximation leads to a satisfiable formula, the computation restarts using more constraints and the previously computed approximation is not reused. Though the new formula eliminates spurious counterexamples of a certain length, there is no guarantee that the subsequent approximation is better than the one previously computed. We take an abstract, approximation-oriented view of interpolation based model checking. We study counterexample-free approximations, which are neither over- nor under-approximations of the set of reachable states but still contain enough information to conclude if counterexamples exist. Using such approximations, we devise a model checking algorithm for approximation refinement and discuss a preliminary implementation of this technique on some hardware benchmarks.
Details
| Address |
Heidelberg‚ Germany |
| Book Title |
Proceedings of the International Conference on Verification‚ Model Checking‚ and Abstract Interpretation (VMCAI) |
| Copyright |
2008 |
| Editor |
Francesco Logozzo and Doron Peled and Lenore D. Zuck |
| ISBN |
978−3−540−78162−2 |
| ISSN |
0302−9743 |
| Month |
January |
| Pages |
68–82 |
| Publisher |
Springer |
| Series |
Lecture Notes in Computer Science |
| Volume |
4905 |
| Year |
2008 |
Links
DOI (10.1007/978-3-540-78163-9)
Related pages
|
People |