research-article

Hybrid CEGAR: combining variable hiding and predicate abstraction

Authors:

Aarti GuptaAuthors Info & Claims

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

Pages 310 - 317

Published: 05 November 2007 Publication History

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]

T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In Programming Language Design and Implementation (PLDI'01), pages 203--213, June 2001.

Digital Library

[3]

T. Ball, A. Podelski, and S. K. Rajamani. Boolean and cartesian abstraction for model checking c programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), pages 268--283. Springer, 2001. LNCS 2031.

Digital Library

[4]

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification (CAV'00), pages 154--169. Springer, 2000. LNCS 1855.

Digital Library

[5]

E. Clarke, A. Gupta, J. Kukula, and O. Strichman. SAT based abstraction-refinement using ILP and machine learning. In E. Brinksma and K. G. Larsen, editors, Computer Aided Verification (CAV'02), pages 265--279. Springer-Verlag, July 2002. LNCS 2404.

Digital Library

[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]

S. Das and D. L. Dill. Successive approximation of abstract transition relations. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS'01), pages 51--58, Boston, MA, June 2001.

Digital Library

[8]

S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In Computer Aided Verification (CAV'97), pages 72--83. Springer, 1997. LNCS 1254.

Digital Library

[9]

A. Gupta, M. Ganai, Z. Yang, and P. Ashar. Iterative abstraction using SAT-based BMC with proof analysis. In International Conference on Computer-Aided Design, pages 416--423, Nov. 2003.

Digital Library

[10]

A. Gupta, M. K. Ganai, and P. Ashar. Lazy constraints and SAT heuristics for proof-based abstraction. In Proceedings of International Conference on VLSI Design, pages 183--188, Jan. 2005.

Digital Library

[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.

Digital Library

[12]

H. Jain, D. Kroening, N. Sharygina, and E. Clarke. Word level predicate abstraction and refinement for verifying RTL verilog. In ACM/IEEE Design Automation Conference (DAC'05), pages 445--450, New York, NY, USA, 2005. ACM Press.

Digital Library

[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.

Digital Library

[14]

D. Kroening and N. Sharygina. Image computation and predicate refinement for RTL verilog using word level proofs. In Design, Automation and Test in Europe (DATE'07), Mar. 2007.

Digital Library

[15]

R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.

Digital Library

[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.

Digital Library

[18]

D. E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie-Mellon University, July 1993.

Digital Library

[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.

Digital Library

[20]

A. Pnueli. The temporal logic of programs. In IEEE Symposium on Foundations of Computer Science, pages 46--57, Providence, RI, 1977.

Digital Library

[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]

C. Wang, B. Li, H. Jin, G. D. Hachtel, and F. Somenzi. Improving Ariadne's bundle by following multiple threads in abstraction refinement. In International Conference on Computer-Aided Design, pages 408--415, Nov. 2003.

Digital Library

[24]

L. Zhang, M. R. Prasad, M. S. Hsiao, and T. Sidle. Dynamic abstraction using SAT-based BMC. In ACM/IEEE Design Automation Conference (DAC'05), pages 754--757, San Jose, CA, June 2005.

Digital Library

Cited By

Luckeneder CKaindl HHung CPapadopoulos G(2019)A case study of systematic top-down design of cyber-physical models with integrated validation and formal verificationProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297460(1828-1836)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297460
Lin CLiu LVasudevan SAyala JJones AMadden PCoskun A(2013)Generating concise assertions with complete coverageProceedings of the 23rd ACM international conference on Great lakes symposium on VLSI10.1145/2483028.2483088(185-190)Online publication date: 2-May-2013
https://dl.acm.org/doi/10.1145/2483028.2483088
Liu LLin CVasudevan SHu A(2012)Word level feature discovery to enhance quality of assertion miningProceedings of the International Conference on Computer-Aided Design10.1145/2429384.2429424(210-217)Online publication date: 5-Nov-2012
https://dl.acm.org/doi/10.1145/2429384.2429424
Show More Cited By

Hybrid CEGAR: combining variable hiding and predicate abstraction
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Hybrid automata-based CEGAR for rectangular hybrid systems

In this paper, we present a counterexample guided abstraction refinement (CEGAR) framework for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we ...
Induction in CEGAR for Detecting Counterexamples
FMCAD '07: Proceedings of the Formal Methods in Computer Aided Design

Induction has been studied in model checking for proving the validity of safety properties, i.e., showing the absence of counterexamples. To our knowledge, induction has not been used to refute safety properties. Existing algorithms including bounded ...
CEGAR based bounded model checking of discrete time hybrid systems
HSCC'07: Proceedings of the 10th international conference on Hybrid systems: computation and control

Many hybrid systems can be conveniently modeled as Piece-wise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem.

We ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

November 2007

933 pages

ISBN:1424413826

General Chair:
Georges Gielen
ESAT-MICAS, Katholieke Univ. Leuven, Leuven, Belgium

Sponsors

CEDA: Council on Electronic Design Automation
SIGDA: ACM Special Interest Group on Design Automation
IEEE CASS/CANDE
IEEE-CS\DATC: IEEE Computer Society

Publisher

IEEE Press

Publication History

Published: 05 November 2007

Check for updates

Qualifiers

Research-article

Conference

ICCAD07

Sponsor:

CEDA
SIGDA
IEEE-CS\DATC

ICCAD07: The International Conference on Computer-Aided Design 2007

November 5 - 8, 2007

California, San Jose

Acceptance Rates

ICCAD '07 Paper Acceptance Rate 139 of 510 submissions, 27%;

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
215
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Luckeneder CKaindl HHung CPapadopoulos G(2019)A case study of systematic top-down design of cyber-physical models with integrated validation and formal verificationProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297460(1828-1836)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297460
Lin CLiu LVasudevan SAyala JJones AMadden PCoskun A(2013)Generating concise assertions with complete coverageProceedings of the 23rd ACM international conference on Great lakes symposium on VLSI10.1145/2483028.2483088(185-190)Online publication date: 2-May-2013
https://dl.acm.org/doi/10.1145/2483028.2483088
Liu LLin CVasudevan SHu A(2012)Word level feature discovery to enhance quality of assertion miningProceedings of the International Conference on Computer-Aided Design10.1145/2429384.2429424(210-217)Online publication date: 5-Nov-2012
https://dl.acm.org/doi/10.1145/2429384.2429424
Yeh HWu CHuang CPhillips JHu AGraeb H(2011)Property-specific sequential invariant extraction for SAT-based unbounded model checkingProceedings of the International Conference on Computer-Aided Design10.5555/2132325.2132475(674-678)Online publication date: 7-Nov-2011
https://dl.acm.org/doi/10.5555/2132325.2132475
Yang ZSakallah K(2010)Trace-driven verification of multithreaded programsProceedings of the 12th international conference on Formal engineering methods and software engineering10.5555/1939864.1939898(404-419)Online publication date: 17-Nov-2010
https://dl.acm.org/doi/10.5555/1939864.1939898

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten