# zbMATH — the first resource for mathematics

SAT-based model checking. (English) Zbl 1392.68232
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 277-303 (2018).
Summary: Modern satisfiability (SAT) solvers have become the enabling technology of many model checkers. In this chapter, we will focus on those techniques most relevant to industrial practice. In bounded model checking (BMC), a transition system and a property are jointly unwound for a given number $$k$$ of steps to obtain a formula that is satisfiable if there is a counterexample for the property up to length $$k$$. The formula is then passed to an efficient SAT solver. The strength of BMC is refutation: BMC has been used to discover subtle flaws in digital systems. We cover the application of BMC to both hardware and software systems, and to hardware/software co-verification. We also discuss means to make BMC complete, including $$k$$-induction, Craig interpolation, abstraction refinement techniques, and inductive techniques with iterative strengthening.
For the entire collection see [Zbl 1390.68001].

##### MSC:
 68Q60 Specification and verification (program logics, model checking, etc.) 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: