Formal Methods in Computer Aided Design (2007)
Austin, Texas, USA
Nov. 11, 2007 to Nov. 14, 2007
Scaling verification to large circuits requires some form of abstraction relative to the asserted property. We describe a safety analysis of finite-state systems that generalizes from counterexamples to the inductiveness of the safety specification to inductive invariants. It thus abstracts the system?s state space relative to the property. The analysis either strengthens a safety specification to be inductive or discovers a counterexample to its correctness. The analysis is easily made parallel. We provide experimental data showing how the analysis time decreases with the number of processes on several hard problems.
Z. Manna and A. R. Bradley, "Checking Safety by Inductive Generalization of Counterexamples to Induction," Formal Methods in Computer Aided Design(FMCAD), Austin, Texas, USA, 2007, pp. 173-180.