Interpolant learning and reuse in SAT-based model checking

DOI10.1016/J.ENTCS.2006.12.021MaRDI QIDQ2864382zbMATH OpenOpenAlexFDO

Authors Joao Marques-Silva

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

zbMATH Keywords

Boolean satisfiabilitybounded model checkinginterpolants

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Interpolation Properties and SAT-Based Model Checking
• Interpolation and SAT-based model checking.
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
• Model checking, synthesis, and learning
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Interpolants and Symbolic Model Checking
• Model learning as a satisfiability modulo theories problem

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A structure-preserving clause form translation
• BerkMin: A fast and robust SAT-solver
• Correct Hardware Design and Verification Methods
• scientific article; zbMATH DE number 1629965 (Why is no real title available?)
• scientific article; zbMATH DE number 1670796 (Why is no real title available?)
• scientific article; zbMATH DE number 1956569 (Why is no real title available?)
• scientific article; zbMATH DE number 1956580 (Why is no real title available?)
• scientific article; zbMATH DE number 1979542 (Why is no real title available?)
• scientific article; zbMATH DE number 1796153 (Why is no real title available?)
• scientific article; zbMATH DE number 1903357 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Temporal induction by incremental SAT solving
• Theory and Applications of Satisfiability Testing

Cited in

(9)

• Fast interpolating BMC
• Incremental design-space model checking via reusable reachable state approximations
• A BDD-Based Algorithm for Learning from Interpretation Transition
• Intertwined forward-backward reachability analysis using interpolants
• Approximation Refinement for Interpolation-Based Model Checking
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Interpolation and SAT-based model checking.
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
• Efficient generation of small interpolants in CNF

Describes a project that uses

Uses Software

• BerkMin
• MiniSat

This page was built for publication: Interpolant learning and reuse in SAT-based model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864382)