Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
From MaRDI portal
Recommendations
Cites work
- An abstraction algorithm for the verification of level-sensitive latch-based netlists
- Approximation Refinement for Interpolation-Based Model Checking
- Benchmarking a model checker for algorithmic improvements and tuning for performance
- Computer Aided Verification
- Computer Aided Verification
- Correct Hardware Design and Verification Methods
- Counterexample-guided abstraction refinement for symbolic model checking
- scientific article; zbMATH DE number 1670775 (Why is no real title available?)
- Interpolant strength
- Interpolation and SAT-based model checking.
- Intertwined forward-backward reachability analysis using interpolants
- Optimization techniques for Craig interpolant compaction in unbounded model checking
- Properties preserved in subdirect products
- SAT-Based Model Checking without Unrolling
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Tools and Algorithms for the Construction and Analysis of Systems
Cited in
(6)- Interpolant learning and reuse in SAT-based model checking
- Tools and Algorithms for the Construction and Analysis of Systems
- Interpolating strong induction
- Searching for i-good lemmas to accelerate safety model checking
- A theorem prover based approach for SAT-based model checking certification
- Optimization techniques for Craig interpolant compaction in unbounded model checking
This page was built for publication: Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6102162)
