Hybrid CEGAR: combining variable hiding and predicate abstraction

ABSTRACT

Variable hiding and predicate abstraction are two popular abstraction methods to obtain simplified models for model checking. Although both methods have been used successfully in practice, no attempt has been made to combine them in counterexample guided abstraction refinement (CEGAR). In this paper, we propose a hybrid abstraction method that allows both visible variables and predicates to take advantages of their relative strengths. We use refinement based on weakest preconditions to add new predicates, and under certain conditions trade in the predicates for visible variables in the abstract model. We also present heuristics for improving the overall performance, based on static analysis to identify useful candidates for visible variables, and use of lazy constraints to find more effective unsatisfiable cores for refinement. We have implemented the proposed hybrid CEGAR procedure. Our experiments on public benchmarks show that the new abstraction method frequently outperforms the better of the two existing abstraction methods.

REFERENCES

• 1: N. Amla and K. L. McMillan. A hybrid of counterexample-based and proof-based abstraction. In Formal Methods in Computer Aided Design (FMCAD'04), pages 260--274, Nov. 2004.
• 2: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 3: Thomas Ball , Andreas Podelski , Sriram K. Rajamani, Boolean and Cartesian Abstraction for Model Checking C Programs, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.268-283, April 02-06, 2001
• 4: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 5: Edmund M. Clarke , Anubhav Gupta , James H. Kukula , Ofer Shrichman, SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques, Proceedings of the 14th International Conference on Computer Aided Verification, p.265-279, July 27-31, 2002
• 6: E. Clarke, M. Talupur, H. Veith, and D. Wang. SAT based predicate abstraction for hardware verification. In International Conference on Theory and Applications of Satisfiability Testing, S. Margherita Ligure, Italy, May 2003.
• 7: Satyaki Das , David L. Dill, Successive Approximation of Abstract Transition Relations, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.51, June 16-19, 2001
• 8: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 9: Aarti Gupta , Malay Ganai , Zijiang Yang , Pranav Ashar, Iterative Abstraction using SAT-based BMC with Proof Analysis, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.416, November 09-13, 2003 [doi>10.1109/ICCAD.2003.87]
• 10: Aarti Gupta , Malay Ganai , Pranav Ashar, Lazy Constraints and SAT Heuristics for Proof-Based Abstraction, Proceedings of the 18th International Conference on VLSI Design held jointly with 4th International Conference on Embedded Systems Design, p.183-188, January 03-07, 2005 [doi>10.1109/ICVD.2005.114]
• 11: H. Jain, F. Ivančić, A. Gupta, and M. Ganai. Localization and register sharing for predicate abstraction. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), pages 394--409. Springer, 2005. LNCS 3440.
• 12: Himanshu Jain , Daniel Kroening , Natasha Sharygina , Edmund Clarke, Word level predicate abstraction and refinement for verifying RTL verilog, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065697]
• 13: H. Jain, D. Kroening, N. Sharygina, and E. Clarke. VCEGAR: Verilog counterexample guided abstraction refinement. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), Mar. 2007.
• 14: Daniel Kroening , Natasha Sharygina, Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
• 15: R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.
• 16: S. K. Lahiri, R. E. Bryant, and B. Cook. A symbolic approach to predicate abstraction. In W. A. Hunt, Jr. and F. Somenzi, editors, Computer Aided Verification (CAV'03), pages 141--153. Springer-Verlag, Berlin, July 2003. LNCS 2725.
• 17: B. Li, C. Wang, and F. Somenzi. Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. Software Tools for Technology Transfer, 2(7):143--155, 2005.
• 18: David Esley Long , Edmund M. Clarke, Model checking, abstraction, and compositional verification, Carnegie Mellon University, Pittsburgh, PA, 1993
• 19: K. L. McMillan and N. Amla. Automatic abstraction without counterexamples. In Tools and Algorithms for Construction and Analysis of Systems (TACAS'03), pages 2--17. Springer, 2003. LNCS 2619.
• 20: A. Pnueli. The temporal logic of programs. In IEEE Symposium on Foundations of Computer Science, pages 46--57, Providence, RI, 1977.
• 21: F. Somenzi. CUDD: CU Decision Diagram Package. University of Colorado at Boulder, ftp://vlsi.colorado.edu/pub/.
• 22: VIS verification benchmarks. http://vlsi.colorado.edu/~vis.
• 23: Chao Wang , Bing Li , HoonSang Jin , Gary D. Hachtel , Fabio Somenzi, Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.408, November 09-13, 2003 [doi>10.1109/ICCAD.2003.83]
• 24: Liang Zhang , Mukul R. Prasad , Michael S. Hsiao , Thomas Sidle, Dynamic abstraction using SAT-based BMC, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065776]