Efficient generation of small interpolants in CNF

DOI10.1007/S10703-015-0224-5zbMATH Open1341.68119OpenAlexW2055440714MaRDI QIDQ746773FDOQ746773

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

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

zbMATH Keywords

interpolationmodel checkingSATvariable elimination

Mathematics Subject Classification ID

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

Cites Work

• Theory and Applications of Satisfiability Testing
• Interpolant strength
• Interpolation and SAT-based model checking.
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• A Computing Procedure for Quantification Theory
• Efficient Generation of Small Interpolants in CNF
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Abstractions from proofs
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Computer Aided Verification
• Lazy Abstraction with Interpolants
• An efficient and flexible approach to resolution proof reduction
• Title not available (Why is that?)
• Interpolant learning and reuse in SAT-based model checking
• Intertwined forward-backward reachability analysis using interpolants

Cited In (2)

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

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)