Efficient generation of small interpolants in CNF

DOI10.1007/S10703-015-0224-5MaRDI QIDQ746773zbMATH OpenOpenAlexFDO

Authors Yakir Vizel, Alexander Nadel, Vadim Ryvchin

Publication date 20 October 2015

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-015-0224-5

zbMATH Keywords

interpolationmodel checkingSATvariable elimination

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Efficient Generation of Small Interpolants in CNF
• Computer Science Logic
• Interpolation and SAT-based model checking.
• Approximation Refinement for Interpolation-Based Model Checking
• Interpolants and Symbolic Model Checking

Cites work

• A Computing Procedure for Quantification Theory
• Abstractions from proofs
• An efficient and flexible approach to resolution proof reduction
• Computer Aided Verification
• Efficient Generation of Small Interpolants in CNF
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• scientific article; zbMATH DE number 1956569 (Why is no real title available?)
• Interpolant learning and reuse in SAT-based model checking
• Interpolant strength
• Interpolation and SAT-based model checking.
• Intertwined forward-backward reachability analysis using interpolants
• Lazy Abstraction with Interpolants
• 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

Cited in

(3)

• Fast interpolating BMC
• Efficient Generation of Small Interpolants in CNF
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

Describes a project that uses

Uses Software

• MiniSat

This page was built for publication: Efficient generation of small interpolants in CNF

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