Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs

DOI10.1007/978-3-642-14186-7_17zbMath1306.68168OpenAlexW1495288201MaRDI QIDQ4930589

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

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

blackboxCraig interpolationQBFSATBMCunsat-core

Mathematics Subject Classification ID

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

Related Items (3)

The QBF Gallery: behind the scenes ⋮ Preservation of Craig interpolation by the product of matrix logics ⋮ Craig interpolation in the presence of unreliable connectives

This page was built for publication: Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs