Name
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-78163-9 | VMCAI |
Keywords | Field | DocType |
computed approximation,counterexample-free approximation,model checking,effective method,new formula,subsequent approximation,reachable state,model checking algorithm,sat solver,interpolation-based model checking,approximation refinement,satisfiability | Abstraction model checking,Model checking,Computer science,Interpolation,Boolean satisfiability problem,Algorithm,Theoretical computer science,Mathematical proof,Counterexample,Spurious relationship,Computation | Conference |
Volume | ISSN | ISBN |
4905 | 0302-9743 | 3-540-78162-5 |
Citations | PageRank | References |
10 | 0.65 | 21 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vijay D'Silva | 1 | 239 | 14.07 |
| Mitra Purandare | 2 | 81 | 5.49 |
| Daniel Kroening | 3 | 3084 | 187.60 |