Bounded model checking (BMC) is a highly successful bug-finding method that uses efficient SAT solvers to examine paths of bounded length for violations of a given specification. A completeness threshold for a given model M and specification is a bound k such that, if no counterexample of length k or less can be found in M, then M in fact satisfies the specification. The quest for ‘small’ completeness thresholds in BMC goes back to the very inception of the technique, over a decade ago, and remains a topic of active research. Language SK/EN, 30+ minutes