Temporal Induction by Incremental SAT Solving

Abstract

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.