Incremental preprocessing methods for use in BMC

DOI10.1007/S10703-011-0122-4MaRDI QIDQ453488zbMATH OpenOpenAlexFDO

Authors Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd Becker

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

BMCCraig interpolationmodel checkingpreprocessingSAT

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)

Recommendations

• Preprocessing in incremental SAT
• Verification of partial designs using incremental QBF
• Ultimately incremental SAT
• An incremental algorithm to check satisfiability for bounded model checking
• Theory and Applications of Satisfiability Testing

Cites work

• A Computing Procedure for Quantification Theory
• Accelerating bounded model checking of safety properties
• Bounded model checking using satisfiability solving
• Interpolant strength
• Interpolation and SAT-based model checking.
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• On a generalization of extended resolution
• Temporal induction by incremental SAT solving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Tutorial on Model Checking: Modelling and Verification in Computer Science
• Unification theory

Cited in

(5)

• Incremental inprocessing in SAT solving
• Preprocessing in incremental SAT
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Theory and Applications of Satisfiability Testing
• Satisfiability modulo user propagators

Describes a project that uses

Uses Software

• MiniSat
• NiVER

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

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