Optimization techniques for Craig interpolant compaction in unbounded model checking
From MaRDI portal
Publication:888467
DOI10.1007/s10703-015-0229-0zbMath1341.68117OpenAlexW2027979159MaRDI QIDQ888467
Danilo Vendraminetto, Carmelo Loiacono, Gianpiero Cabodi
Publication date: 30 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-0229-0
Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)
Related Items (3)
Optimization techniques for Craig interpolant compaction in unbounded model checking ⋮ Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking ⋮ Exploiting partial variable assignment in interpolation-based model checking
Uses Software
Cites Work
- Unnamed Item
- Benchmarking a model checker for algorithmic improvements and tuning for performance
- Resolution proof transformation for compression and interpolation
- Properties preserved in subdirect products
- Optimization techniques for Craig interpolant compaction in unbounded model checking
- Efficient Generation of Small Interpolants in CNF
- SAT-Based Model Checking without Unrolling
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Improved Single Pass Algorithms for Resolution Proof Reduction
- Two Techniques for Minimizing Resolution Proofs
- Compression of Propositional Resolution Proofs via Partial Regularization
- Theory and Applications of Satisfiability Testing
- An Efficient and Flexible Approach to Resolution Proof Reduction
- Approximation Refinement for Interpolation-Based Model Checking
- Correct Hardware Design and Verification Methods
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Computer Aided Verification
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
This page was built for publication: Optimization techniques for Craig interpolant compaction in unbounded model checking
