Bounded model checking is employed in tools for the formal verification of C programs such as the C bounded model checker (CBMC). The key idea of this technique is to unwind unbounded program loops to a fixed depth and to translate the resulting program into a formula whose satisfiability (determined by a Boolean satisfiability problem/satisfiability modulo theory (SAT/SMT) solver) indicates a runtime error or the failure of a safety property, respectively. Confidence in the program is established by checking programs for growing unwinding depths yielding growing formulas to be solved; this, however, is wasteful because it repeats work from solving previous formulas.

This paper capitalizes on recent advances in incremental SAT solving, which is able to reuse work spent on solving smaller formulas for solving extended formulas. Specifically, it demonstrates how the formulas derived from time-triggered systems such as automotive embedded systems (which only contain a single unbounded loop) are amenable to a formula encoding in which the problem of non-monotonic formula extensions is addressed by additional Boolean variables that “switch off” clauses from previously checked formulas; furthermore, this technique does not interfere with SAT optimization techniques like symbolic execution and slicing.

The paper clearly illustrates the core ideas also for nonexperts and demonstrates their advantages by benchmarking an extended version of CBMC on various industrial programs from the automotive industry; for these, with incremental checking, a speedup in the range of five to ten times can be achieved. The demonstrated results are promising with possible extensions to improve its performance and range of applicability, for example, to concurrent programs.