Efficient generation of small interpolants in CNF

DOI10.1007/s10703-015-0224-5zbMath1341.68119OpenAlexW2055440714MaRDI QIDQ746773

Vadim Ryvchin, Alexander Nadel, Yakir Vizel

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 checkingvariable eliminationSAT

Mathematics Subject Classification ID

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

Uses Software

• MiniSat

Cites Work

• Unnamed Item
• Interpolant Learning and Reuse in SAT-Based Model Checking
• Efficient Generation of Small Interpolants in CNF
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Abstractions from proofs
• Interpolant Strength
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Intertwined Forward-Backward Reachability Analysis Using Interpolants
• An Efficient and Flexible Approach to Resolution Proof Reduction
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification
• Lazy Abstraction with Interpolants
• Computer Aided Verification

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