Interpolant Learning and Reuse in SAT-Based Model Checking
From MaRDI portal
Publication:2864382
DOI10.1016/j.entcs.2006.12.021zbMath1277.68140OpenAlexW2129952473MaRDI QIDQ2864382
Publication date: 6 December 2013
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2006.12.021
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (4)
Incremental design-space model checking via reusable reachable state approximations ⋮ Approximation Refinement for Interpolation-Based Model Checking ⋮ Efficient Interpolant Generation in Satisfiability Modulo Theories ⋮ Efficient generation of small interpolants in CNF
Uses Software
Cites Work
- A structure-preserving clause form translation
- BerkMin: A fast and robust SAT-solver
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Theory and Applications of Satisfiability Testing
- Correct Hardware Design and Verification Methods
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Computer Aided Verification
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Interpolant Learning and Reuse in SAT-Based Model Checking
