Bounded Model Checking

← Back to document page

P02c00 bmc 2008/11/20 10:13 page 457 #3 Handbook of SatisfiabilityArmin Biere, Marijn Heule, Hans van Maaren and Toby Walsh (Eds.)IOS Press, 2009c 2009 Armin Biere and IOS Press. All rights 14Bounded Model CheckingArmin BiereBesides Equivalence Checking [KK97, KPKG02] the most important indus-trial application of SAT is currently Bounded Model Checking (BMC) [BCCZ99].Both techniques are used forformalhardware verification in the context of elec-tronic design automation (EDA), but have successfully been applied to manyother domains as well. In this chapter, we focus on practice, BMC is mainly used for falsification resp. testing, which is con-cerned with violations of temporal properties.

the same principles as plain BMC. Two further related applications, in which BMC becomes more and more ... SAT-based model checking, at least for falsification, scales much better [Kur08]. Another important direction in model checking is explicit state model check-ing. The SPIN model checker [Hol04] is the most prominent explicit state model

  Applications, Principles, Model, Check, Checking, Model checking, Model check ing