Temporal Induction by Incremental SAT Solving

We show how a very modest modification to a typical modern SAT-solver enables it to solve a series of related SAT-instances efficiently. We apply this idea to checking safety properties by means of temporal induction, a technique strongly related to bounded model checking. We further give a more efficient way of constraining the extended induction hypothesis to so called loop-free paths. We have also performed the first comprehensive experimental evaluation of induction methods for safety-checking.