Temporal Induction by Incremental SAT Solving
Niklas Eén, Niklas Sörensson · Electronic Notes in Theoretical Computer Science · 2003
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.