Optimization techniques for Craig interpolant compaction in unbounded model checking
type: Item
instance of: scholarly article
title: Optimization techniques for Craig interpolant compaction in unbounded model checking
zbMATH Open document ID: 1341.68117
author: G. Cabodi
author: Carmelo Loiacono
author: Danilo Vendraminetto
published in: Formal Methods in System Design
publication date: 2015-10-30T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03C40
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 94C10
zbMATH DE Number: 6502610
zbMATH Keywords: Craig interpolant
zbMATH Keywords: SAT-based unbounded model checking
zbMATH Keywords: proof reduction
zbMATH Keywords: interpolant reduction
describes a project that uses: ABC
describes a project that uses: Chaff
MaRDI profile type: Publication
full work available at URL: s10703-015-0229-0
OpenAlex ID: W2027979159
cites work: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
cites work: Properties preserved in subdirect products
cites work: Computer Aided Verification
cites work: SAT-Based Model Checking without Unrolling
cites work: Correct Hardware Design and Verification Methods
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Approximation Refinement for Interpolation-Based Model Checking
cites work: A Computing Procedure for Quantification Theory
cites work: A machine program for theorem-proving
cites work: An Efficient and Flexible Approach to Resolution Proof Reduction
cites work: Compression of Propositional Resolution Proofs via Partial Regularization
cites work: Improved Single Pass Algorithms for Resolution Proof Reduction
cites work: Two Techniques for Minimizing Resolution Proofs
cites work: Q4804900
cites work: Benchmarking a model checker for algorithmic improvements and tuning for performance
cites work: Resolution proof transformation for compression and interpolation
cites work: Efficient Generation of Small Interpolants in CNF
cites work: Theory and Applications of Satisfiability Testing
DOI: 10.1007/S10703-015-0229-0
Recommended article: Tools and Algorithms for the Construction and Analysis of Systems
Recommended article: Applications and Theory of Petri Nets 2005
Recommended article: Computer Science Logic
Recommended article: Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs
Recommended article: Unbounded Model-Checking with Interpolation for Regular Language Constraints
Recommended article: Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
Recommended article: Accelerating Interpolation-Based Model-Checking
Recommended article: Q4942016
description: scientific article; zbMATH DE number 6502610