Inductive verification of iterative systems

Recent advances in binary decision diagram (BDD)-based algorithms have brought much larger circuits than before within the reach of verification programs. The authors show how inductive proof procedures can derive information on regular circuits in optimal time, e.g. they can perform reachability analysis in linear time or check the equivalence of two iterative circuits in time independent of the length of the two arrays. The algorithms presented rely on the canonicity of BDDs to make the inductive steps efficient. The authors have experimented with the techniques described and compared them with the conventional techniques on a few examples. >