Bounded model checking

By Armin Biere. Advances in Computing, 2003

1,281 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

A brief account of runtime verification (2009, methodology): “If such a precise model of the underlying system is given, and, if moreover a bound on the size of its state space is known, powerful, so-called bounded model-checking techniques can be applied [13] for analyzing the system.”
Bounded synthesis (2007, methodology): “Inspired by the success of bounded model checking [1,2], we show that the bounded synthesis problem of finding an implementation whose size is bounded by b can be effectively reduced to a SMT problem.”
HAMPI: a solver for string constraints (2009, methodology): “disjunct ()[()() + (())], H creates the following formula: D1a: bv[0] = 40 ∧ bv[1] = 41 ∧ ((bv[2] = 40 ∧ bv[3] = 41 ∧ bv[4] = 40 ∧ bv[5] = 41) ∨ (bv[2] = 40 ∧ bv[3] = 40 ∧ bv[4] = 41 ∧ bv[5] = 41)).”
Automated reasoning (2013, neutral): “…Programming (CP) benchmark problems by compiling them SAT instances and by using encodings can be used to convert a same into SAT, including the direct-encoding, the [86]. solvers are the main workhorse in the area of veriﬁcation of transition systems [19, 20] called Model Checking (BMC).”