Efficient computation of small abstraction refinements

ABSTRACT

In the abstraction refinement approach to model checking, the discovery of spurious counterexamples in the current abstract model triggers its refinement. The proof - produced by a SAT solver - that the abstract counterexamples cannot be concretized can be used to identify the circuit elements or predicates that should be added to the model. It is common, however, for the refinements thus computed to be highly redundant. A costly minimization phase is therefore often needed to prevent excessive growth of the abstract model. In This work we show how to modify the search strategy of a SAT solver so that it generates refinements that are close to minimal, thus greatly reducing the time required for their minimization.

REFERENCES

• 1: [1] B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21:181-185, Oct. 1985.
• 2: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 3: 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: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 4: Pankaj Chauhan , Edmund M. Clarke , James H. Kukula , Samir Sapra , Helmut Veith , Dong Wang, Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.33-51, November 06-08, 2002
• 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: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: Evgueni Goldberg , Yakov Novikov, Verification of Proofs of Unsatisfiability for CNF Formulas, Proceedings of the conference on Design, Automation and Test in Europe, p.10886, March 03-07, 2003
• 8: [8] IBM Formal Verification Benchmarks. URL: http:// www.haifa.il.ibm.com/projects/verification/RB_Homepage/ benchmarks.html.
• 9: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 10: [10] B. Li, C. Wang, and F. Somenzi. A satisfiability-based approach to abstraction refinement in model checking. Electronic Notes in Theoretical Computer Science, 89(4), 2003. First International Workshop on Bounded Model Checking. http://www.elsevier.nl/locate/entcs/volume89.html.
• 11: [11] 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, 2004. Submitted for publication.
• 12: [12] I. Lynce and J. P. Marques-Silva. On computing minimum unsatisfiable cores. In International Conference on Theory and Applications of Satisfiabilily Testing (SAT 2004), Vancouver, Canada, May 2004.
• 13: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 14: [14] K. L. McMillan and N. Amla. Automatic abstraction without counterexamples. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03), pages 2-17, Warsaw, Poland, Apr. 2003. LNCS 2619.
• 15: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 16: Yoonna Oh , Maher N. Mneimneh , Zaher S. Andraus , Karem A. Sakallah , Igor L. Markov, AMUSE: a minimally-unsatisfiable subformula extractor, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996710]
• 17: 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
• 18: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 19: [19] URL: http://vlsi.colorado.edu/~vis.
• 20: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 21: Lintao Zhang , Sharad Malik, Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications, Proceedings of the conference on Design, Automation and Test in Europe, p.10880, March 03-07, 2003