Automated abstraction by incremental refinement in interpolant-based model checking

ABSTRACT

This paper addresses the field of Unbounded Model Checking (UMC) based on SAT engines, where Craig interpolants have recently gained wide acceptance as an automated abstraction technique.

We start from the observation that interpolants can be quite effective on large verification instances. As they operate on SAT-generated refutation proofs, interpolants are very good at automatically abstract facts that are not significant for proofs. In this work, we push forward the new idea of generating abstractions without resorting to SAT proofs, and to accept (reject) abstractions whenever they (do not) fulfill given adequacy constraints. We propose an integrated approach smoothly combining the capabilities of interpolation with abstraction and over-approximation techniques, that do not directly derive from SAT refutation proofs.

The driving idea of this combination is to incrementally generate, by refinement, an abstract (over-approximate) image, built up from equivalences, implications, ternary and localization abstraction, then (eventually) from SAT refutation proofs.

Experimental results, derived from the verification of hard problems, show the robustness of our approach.

REFERENCES

• 1: J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill, "Symbolic Model Checking for Sequential Circuit Verification," IEEE Trans. on Computer-Aided Design, vol. 13, no. 4, pp. 401--424, Apr. 1994.
• 2: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 3: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 4: P. Bjesse , A. Boralv, DAG-aware circuit compression for formal verification, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.42-49, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382541]
• 5: Per Bjesse , Koen Claessen, SAT-Based Verification without State Space Traversal, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.372-389, November 01-03, 2000
• 6: M. L. Case, A. Mishchenko, and R. K. Brayton, "Inductively Finding a Reachable State Space Over-Approximation," in Proc. Int'l Workshop on Logic Synthesis, Lake Tahoe, California, May 2006.
• 7: F. Lu and K. T. Cheng, "IChecker: An Efficient Checker for Inductive Invariants," in High-Level Design Validation and Test Workshop, 2006, pp. 176--180.
• 8: Gianpiero Cabodi , Sergio Nocco , Stefano Quer, Boosting the role of inductive invariants in model checking, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
• 9: Mary Sheeran , Satnam Singh , Gunnar Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.108-125, November 01-03, 2000
• 10: Poul Frederick Williams , Armin Biere , Edmund M. Clarke , Anubhav Gupta, Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking, Proceedings of the 12th International Conference on Computer Aided Verification, p.124-138, July 15-19, 2000
• 11: Parosh Aziz Abdulla , Per Bjesse , Niklas Eén, Symbolic Reachability Analysis Based on SAT-Solvers, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.411-425, March 25-April 02, 2000
• 12: Kenneth L. McMillan, Applying SAT Methods in Unbounded Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.250-264, July 27-31, 2002
• 13: Hyeong-Ju Kang , In-Cheol Park, SAT-based unbounded symbolic model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.776043]
• 14: M. K. Ganai , A. Gupta , P. Ashar, Efficient SAT-based unbounded symbolic model checking using circuit cofactoring, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.510-517, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382631]
• 15: K. L. McMillan, "Interpolation and SAT-Based Model Checking," in Proc. Computer Aided Verification, ser. LNCS, W. A. H. Jr. and F. Somenzi, Eds., vol. 2725. Boulder, CO, USA: Springer, 2003, pp. 1--13.
• 16: K. L. McMillan and R. Jhala, "Interpolation and SAT-Based Model Checking," in Proc. Computer Aided Verification, ser. LNCS, T. Ball and R. B. Jones, Eds., vol. 3725. Edimburgh, Scotlan, UK: Springer, 2005, pp. 39--51.
• 17: J. Marques-Silva, "Improvements to the implementation of Interpolant-Based Model Checking," in Proc. Computer Aided Verification, ser. LNCS, D. Borrione and W. Paul, Eds., vol. 3725. Edimburgh, Scotlan, UK: Springer, 2005, pp. 367--370.
• 18: Gianpiero Cabodi , Marco Murciano , Sergio Nocco , Stefano Quer, Stepping forward with interpolants in unbounded model checking, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California [doi>10.1145/1233501.1233661]
• 19: B. Li and F. Somenzi, "Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking," in Tools and Algorithms for the Construction and Analysis of Systems, vol. 3920, 2006, pp. 227--241.
• 20: A. Biere and T. Jussila, "The Model Checking Competition Web Page, http://fmv.jku.at/hwmcc07/organizers.html," 2007.
• 21: A. Biere and T. Jussila, "The Model Checking Competition Web Page, http://fmv.jku.at/hwmcc08/organizers.html," 2008.
• 22: A. B. Y. Bres, G. Berry and E. M. Sentovich, "State Abstraction Techniques for the Verification of Synchronous Circuits," in dcc02: Designing Correct Circuits 2002, Grenoble, France, Apr. 2002.
• 23: S. Malik, "Analysis of Cyclic Combinational Circuits," vol. 13, no. 7, 1994, pp. 950--956.
• 24: Thomas R. Shiple , Gerard Berry , Herve Touati, Constructive Analysis of Cyclic Circuits, Proceedings of the 1996 European conference on Design and Test, p.328, March 11-14, 1996
• 25: Z. Khasidashvili and Z. Hanna, "Sat-based methods for sequential hardware equivalence verification without synchronization," in BMC'03: First International Workshop on Bounded Model Checking, Boulder, Colorado, Jul. 2003, pp. 593--607.
• 26: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.248-256, November 06-08, 1996