Encoding techniques, Craig interpolants and bounded model checking for incomplete designs

DOI10.1007/978-3-642-14186-7_17MaRDI QIDQ4930589zbMATH OpenOpenAlexFDO

Authors Christian R. Miller, Stefan Kupferschmid, Matthew Lewis, Bernd Becker

Publication date 29 September 2010

Published in Theory and Applications of Satisfiability Testing – SAT 2010 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14186-7_17

zbMATH Keywords

blackboxBMCCraig interpolationQBFSATunsat-core

Mathematics Subject Classification ID

Interpolation, preservation, definability (03C40) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Computer Science Logic
• Interpolation and SAT-based model checking.
• Formal Methods in Computer-Aided Design
• Optimization techniques for Craig interpolant compaction in unbounded model checking
• Verification of partial designs using incremental QBF

Cited in

(4)

• Craig interpolation in the presence of unreliable connectives
• Preservation of Craig interpolation by the product of matrix logics
• The QBF Gallery: behind the scenes
• Optimization techniques for Craig interpolant compaction in unbounded model checking

This page was built for publication: Encoding techniques, Craig interpolants and bounded model checking for incomplete designs

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