Incremental preprocessing methods for use in BMC

DOI10.1007/s10703-011-0122-4zbMath1247.68167OpenAlexW2048373673MaRDI QIDQ453488

Stefan Kupferschmid, Bernd Becker, Matthew Lewis, Tobias Schubert

Publication date: 27 September 2012

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-011-0122-4

zbMATH Keywords

model checkingCraig interpolationSATpreprocessingBMC

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)

Related Items (1)

The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1

Uses Software

• MiniSat
• NiVER

Cites Work

• Unnamed Item
• Unnamed Item
• Accelerating bounded model checking of safety properties
• On a generalization of extended resolution
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Tutorial on Model Checking: Modelling and Verification in Computer Science
• Interpolant Strength
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification
• Bounded model checking using satisfiability solving

This page was built for publication: Incremental preprocessing methods for use in BMC