Armin Biere, Daniel Kröning,
"SAT-Based Model Checking"
, Springer, Cham, 5-2018, ISBN: 978-3-319-10575-8
Original Titel:
SAT-Based Model Checking
Sprache des Titels:
Englisch
Original Kurzfassung:
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
k
of steps to obtain a formula that is satisfiable if there is a counterexample for the property up to length
k
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
k
-induction, Craig interpolation, abstraction refinement techniques, and inductive techniques with iterative strengthening.