Approximation Refinement for Interpolation−Based Model Checking
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 co...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2008
|
| _version_ | 1826281525016002560 |
|---|---|
| author | D'Silva, V Purandare, M Kroening, D |
| author2 | Logozzo, F |
| author_facet | Logozzo, F D'Silva, V Purandare, M Kroening, D |
| author_sort | D'Silva, V |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T00:30:06Z |
| format | Conference item |
| id | oxford-uuid:7f78341e-0e36-4ba5-89d5-fb850c27f59c |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:30:06Z |
| publishDate | 2008 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:7f78341e-0e36-4ba5-89d5-fb850c27f59c2022-03-26T21:17:15ZApproximation Refinement for Interpolation−Based Model CheckingConference itemhttp://purl.org/coar/resource_type/c_5794uuid:7f78341e-0e36-4ba5-89d5-fb850c27f59cDepartment of Computer ScienceSpringer2008D'Silva, VPurandare, MKroening, DLogozzo, FPeled, DZuck, LModel 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. |
| spellingShingle | D'Silva, V Purandare, M Kroening, D Approximation Refinement for Interpolation−Based Model Checking |
| title | Approximation Refinement for Interpolation−Based Model Checking |
| title_full | Approximation Refinement for Interpolation−Based Model Checking |
| title_fullStr | Approximation Refinement for Interpolation−Based Model Checking |
| title_full_unstemmed | Approximation Refinement for Interpolation−Based Model Checking |
| title_short | Approximation Refinement for Interpolation−Based Model Checking |
| title_sort | approximation refinement for interpolation based model checking |
| work_keys_str_mv | AT dsilvav approximationrefinementforinterpolationbasedmodelchecking AT purandarem approximationrefinementforinterpolationbasedmodelchecking AT kroeningd approximationrefinementforinterpolationbasedmodelchecking |