REFERENCES

for invariant generation (which is limited by the 300-s bound). Both plots have been drawn, with the instances sorted by growing Y values. We can observe a relevant size compaction in many cases (more than 30 % reduction in about 300 instances), whereas the time overhead is highly acceptable in most cases. (In about 550 of the 653 invariants, computation required less than 150 s.) VI. CONCLUSION This paper has addressed two main issues. It has described opti-mized techniques to speed up the computation of inductive invariants by means of efficient data structures and manipulation algorithms based on equivalence classes. It has then shown how to effectively in-tegrate inductive invariants within state-of-the-art noninductive model-checking procedures. Experimental data show very promising results, improving the results obtained during the 2007 Model Checking Competition