微信服务号

微信订阅号

2025-4-15- 12
Home > Archive>Volume 19, Issue 1, 2008 >27-38
PDF HTML XML Export Cite reminder
Advances in Predicate Abstraction
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [39]
    • |
  • Related [20]
    • |
  • Cited by [11]
    • | |
  • Comments
    Abstract:

    With the growing increase in software/hardware system scale and function, the further development and application of model checking has been greatly limited by state space explosion, which becomes the bottleneck of verifying large industrial designs. Predicate abstraction, as one of the most effective ways to address state explosion, has been fueled over the recent years. This paper presents a survey of the latest developments in predicate abstraction. A basic algorithm for predicate abstraction is introduced first, followed by comparison among several solvers. Emphases are put on counterexample-guided abstraction refinement and interpolation-based abstraction refinement, including the principles and improvements. The qualities of the new predicate generation methods are also analyzed. Finally, the major challenges in making this technology more pervasive in industrial design verification domain are noted.

    Reference
    [1] Susanne G, Hassen S. Construction of abstract state graphs with PVS. In: Grumberg O, ed. Proc. of the 9th Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 1997. 72-83.
    [2] Detlefs D, Nelson G, Saxe JB. Simplify: A theorem prover for program checking. Journal of the ACM, 2005,52(3):365-473.
    [3] Ball T, Cook B, Lahiri SK, Zhang L. Zapato: Automatic theorem proving for predicate abstraction refinement. In: Harald G, ed. Proc. of the 16th Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2004. 457-461.
    [4] Clarke E, Kroening D, Sharygina N, Yorav K. Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design, 2004,25(2):105-127.
    [5] Davis M, Putnam H. A computing procedure for quantification theory. Journal of the ACM, 1960,7(3):201-215.
    [6] Krzysztof R. Some remarks on Boolean constraint propagation. In: Krzysztof R, ed. Proc. of the Joint ERCIM/Compulog Net Workshop on New Trends in Constraints. London: Springer-Verlag, 1999. 91-107.
    [7] Marques-Silva JP, Sakallah KA. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. on Computers, 1999, 48(5):506-521.
    [8] Zhang HT. SATO: An efficient propositional prover. In: Niehren J, ed. Proc. of the 14th Int'l Conf. on Automated Deduction. Berlin: Springer-Verlag, 1997. 272-275.
    [9] Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S. Chaff: Engineering an efficient SAT solver. In: Rabaey J, ed. Proc. of the 38th Design Automation Conf. Las Vegas: ACM Press, 2001. 530-535.
    [10] Wang D. SAT based abstraction refinement for hardware verification [Ph.D. Thesis]. Pittsburgh: Carnegie Mellon University, 2003.
    [11] Clarke E, Grumberg O, Jha S, Lu Y, Weith H. Counterexample-Guided abstraction refinement. In: Emerson EA, ed. Proc. of the 12th Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2000. 154-169.
    [12] Gupta A. Learning abstraction for model checking [Ph.D. Thesis]. Pittsburgh: Carnegie Mellon University, 2006.
    [13] Chauhan P, Clarke E, Kukula J, Sapra S, Veith H, Wang D. Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard MD, ed. Proc. of the 4th Int'l Conf. on Formal Methods in Computer Aided Design. Berlin: Springer-Verlag, 2002. 33-51.
    [14] Li T, Guo Y, Li SK, Liu GJ. Predicate abstraction of RTL verilog descriptions using constraint logic programming. In: Peled DA, ed. Proc. of the 3rd Int'l Symp. on Automated Technology for Verification and Analysis. Berlin: Springer-Verlag, 2005. 174-186.
    [15] Seshia SA, Lahiri SK, Bryant RE. A hybrid sat-based decision procedure for separation logic with uninterpreted functions. In: Fix L, ed. Proc. of the 40th Design Automation Conf. Anaheim: ACM Press, 2003. 425-430.
    [16] Marco B, Roberto B, Alessandro C, Tommi J, Van Rossum P, Stephan S, Roberto S. An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Halbwachs N, ed. Proc. of the 11th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag, 2005. 317-333.
    [17] Marco B, Roberto B, Alessandro C, Tommi J, Silvio R, Van Rossum P, Roberto S. Efficient satisfiability modulo theories via delayed theory combination. In: Etessami K, ed. Proc. of the 17th Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2005. 335-349.
    [18] Shuvendu KL, Robert N, Albert O. SMT techniques for fast predicate abstraction. In: Manolios P, ed. Proc. of the 18th Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2006. 424-437.
    [19] Satyaki D. Predicate abstraction [Ph.D. Thesis]. Stanford University, 2003.
    [20] Mang FYC, Ho P-H. Abstraction refinement by controllability and cooperativeness analysis. In: Martin GE, ed. Proc. of the 41st Design Automation Conf. San Diego: ACM Press, 2004. 224-229.
    [21] Barbara K, Vitali K. Counterexample-Guided abstraction refinement for the analysis of graph transformation systems. In: Hermanns B, ed. Proc. of the 12th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag, 2006. 197-211.
    [22] Biere A, Cimatti A, Clarke EM, Strichman O, Zhu YS. Bounded model checking. Advances in Computers, 2003. 58. http://citeseer.ist.psu.edu/biere03bounded.html
    [23] McMillan KL, Amla N. Automatic abstraction without counterexamples. In: Garavel H, ed. Proc. of the 9th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag, 2003. 2-17.
    [24] Esparza J, Kiefer S, Schwoon S. Abstraction refinement with craig interpolation and symbolic pushdown systems. In: Hermanns H, Palsberg J, eds. Proc. of the 12th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag, 2006. 489-503.
    [25] Amla N, McMillan KL. A hybrid of counterexample-based and proof-based abstraction. In: Alan JH, ed. Proc. of the 5th Int'l Conf. on Formal Methods in Computer-Aided Design. Berlin: Springer-Verlag, 2004. 14-17.
    [26] Biere A, Clarke E, Raimi R, Zhu YS. Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs. In: Halbwachs N, ed. Proc. of the 11th Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 1999. 60-71.
    [27] Shtrichman O. Pruning techniques for the SAT-based bounded model checking problem. In: Margaria T, ed. Proc. of the 11th Advanced Research Working Conf. on Correct Hardware Design and Verification Methods. Berlin: Springer-Verlag, 2001. 58-70.
    [28] Shtrichman O. Tuning SAT checkers for bounded model checking. In: Emerson EA, ed. Proc. of the 12th Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2000. 480-494.
    [29] Baumgartner J, Kuehlmann A, Abraham J. Property checking via structural analysis. In: Barrett CW, ed. Proc. of the 14th Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2002. 151-165.
    [30] Ball T, Rajamani SK. Generating abstract explanations of spurious counterexamples in C programs. Technical Report, MSR-TR-2002-09, Redmond: Microsoft Research, Microsoft Corporation, 2002. http://research.microsoft.com/research/pubs/view. aspx-msr_id=MSR-TR-2002-09
    [31] Chaki S, Clarke E, Groce A, Strichman O. Predicate abstraction with minimum predicates. In: Geist D, ed. Proc. of the 12th Advanced Research Working Conf. on Correct Hardware Design and Verification Methods. Berlin: Springer-Verlag, 2003. 19-34.
    [32] Lakhnech Y, Bensalem S, Berezin S, Owre S. Incremental verification by abstraction. In: Margaria T, ed. Proc. of the 7th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer-Verlag, 2001. 98-112.
    [33] Ball T. Formalizing counterexample-driven refinement with weakest preconditions. Technical Report, MSR-TR-2004-134, Redmond: Microsoft Research, 2004. 1-19.
    [34] Henzinger TA, Jhala R, Majumdar R. Lazy abstraction. In: Bakel SV, ed. Proc. of the ACM Symp. on Principles of Programming Languages. Oregon: ACM Press, 2002. 58-70.
    [35] Flanagan C, Qadeer S. Predicate abstraction for software verification. In: Bakel SV, ed. Proc. of the ACM Symp. on Principles of Programming Languages. Oregon: ACM Press, 2002. 191-202.
    [36] Chaki SJ. A counterexample guided abstraction refinement framework for verifying concurrent C programs [Ph.D. Thesis]. Pittsburgh: Carnegie Mellon University, 2005.
    [37] Ball T, Majumdar R, Millstein T, Rajamani SK. Automatic predicate abstraction of c programs. In: Soffa ML, ed. Proc. of the 2001 ACM SIGPLAN Conf. on Programming Language Design and Implementation. Snowbird: ACM Press, 2001.
    [38] Clarke E, Jain H, Kroening D. Predicate abstraction and refinement techniques for verifying verilog. Technical Report, CMU-CS-04-139, Pittsburgh: Camegie Mellon University, 2004.
    [39] Wang C, Hachtel GD, Somenzi F. Fine-Grain abstraction and sequential don't cares for large scale model checking. In: Greenberg H, ed. Proc. of the IEEE Int'l Conf. on Computer Design: VLSI in Computers & Processors. Los Alamitos: IEEE Computer Society, 2004. 112-118.
    Comments
    Comments
    分享到微博
    Submit
Get Citation

屈婉霞,李 暾,郭 阳,杨晓东.谓词抽象技术研究.软件学报,2008,19(1):27-38

Copy
Share
Article Metrics
  • Abstract:7885
  • PDF: 9463
  • HTML: 0
  • Cited by: 0
History
  • Received:September 12,2006
  • Revised:May 10,2007
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2035125Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063