Article

Accelerating high-level bounded model checking

Authors:

Aarti GuptaAuthors Info & Claims

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

Pages 794 - 801

https://doi.org/10.1145/1233501.1233664

Published: 05 November 2006 Publication History

Abstract

SAT-based Bounded Model Checking (BMC) has been found promising in finding deep bugs in industry designs and scaling well with design sizes. However, it has limitations due to requirement of finite data paths, inefficient translations and loss of high-level design information during the BMC problem formulation. These shortcomings inherent in Boolean-level BMC can be avoided by using high-level BMC. We propose a novel framework for high-level BMC, which includes several techniques that extract high-level design information from EFSM models to make the verification model "BMC friendly", and use it on-the-fly to simplify the BMC problem instances. Such techniques overcome the inherent limitations of Boolean-level BMC, while allowing integration of state-of-the-art techniques for BMC. In our controlled experiments we found signficant performance improvements achievable by the proposed techniques.

References

[1]

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, "Symbolic model checking using SAT procedures instead of BDDs," in Proceedings of the DAC, 1999.

Digital Library

[2]

M. Sheeran, S. Singh, and G. Stalmarck, "Checking Safety Properties using Induction and a SAT Solver," in Proceedings of Conference on FMCAD, 2000.

Digital Library

[3]

O. Strichman, "Pruning Techniques for the SAT-based bounded model checking," in Proceedings of TACAS, 2001.

[4]

M. Ganai, A. Gupta, and P. Ashar, "DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems," in Proceeding of TACAS, 2005.

Digital Library

[5]

L. Zhang and S. Malik, "The Quest for Efficient Boolean Satisfiability Solvers," in Proceeding of CAV, 2002.

Digital Library

[6]

H. Andersen and H. Hulgard, "Boolean expression diagram," in Proceeding of LICS, 1997.

Digital Library

[7]

M. Ganai and A. Aziz, "Improved SAT-based Bounded Reachability Analysis," in Proceedings of VLSI Design Conference, 2002.

Digital Library

[8]

J. Whittemore, J. Kim, and K. Sakallah, "SATIRE: A New Incremental Satisfiability Engine," Proceedings of DAC, 2001.

Digital Library

[9]

K. L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem: Kluwer Academic Publishers, 1993.

[10]

M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. V. Rossum, M. Schulz, and R. Sebastiani, "The MathSAT 3 System," in Proceedings of CADE, 2005.

Digital Library

[11]

C. Barrett, D. L. Dill, and J. Levitt, "Validity Checking for Combination of Theories with Equality," in Proceedings of FMCAD, 1996.

Digital Library

[12]

R. E. Bryant, S. K. Lahiri, and S. A. Seshia, "Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions," in CAV, 2002.

Digital Library

[13]

R. Nieuwenhuis and A. Oliveras, "DPLL(T) with Exhaustive Theory Propogation and its Application to Difference Logic," in CAV, 2005.

Digital Library

[14]

C. Wang, F. Ivancic, M. Ganai, and A. Gupta, "Deciding Separation Logic Formulae with SAT by Incremental Negative Cycle Elimination," in Proceeding of Logic for Programming, Artificial Intelligence and Reasoning, 2005.

Digital Library

[15]

M. Ganai, M. Talupur, and A. Gupta, "SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver," 2006.

[16]

L. d. Moura, H. RueB, and M. Sorea, "Lazy Theorem Proving for Bounded Model Checking over Infinite Domains," in Proceedings of CADE, 2002.

Digital Library

[17]

A. Armando, J. Mantovani, and L. Platania, "Bounded Model Checking of Software using SMT Solvers instead of SAT solvers," University of Genova 2005.

[18]

M. R. Prasad, A. Biere, and A. Gupta, "A survery of recent advances in SAT-based formal verification.," in STTT 7(2), 2005.

[19]

A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques and Tools: Addison-wesley Publishing Company, 1988.

Digital Library

[20]

M. Ganai and A. Kuehlmann, "On-the-Fly Compression of Logical Circuits," in Proceedings of International Workshop on Logic Synthesis, 2000.

[21]

J.-C. Filliatre, S. Owre, H. RueB, and N. Shankar, "ICS: Integrated Canonizer and Solver," in Proceedings of CAV, 2001.

Digital Library

[22]

M. Ganai, A. Gupta, and P. Ashar, "Beyond Safety: Customized SAT-based Model Checking," in Proceeding of DAC, 2005.

Digital Library

[23]

B. Korel, I. Singh, L. Tahat, and B. Vaysburg, "Slicing of State-based Models," in Proceedings of ICSM, 2003.

Digital Library

[24]

F. Ivancic, J. Yang, M. Ganai, A. Gupta, and P. Ashar, "Efficient SAT-based Bounded Model Checking for Software," in Proceedings of ISOLA, 2004.

[25]

H. Jain, F. Ivancic, A. Gupta, I. Shlyakhter, and C. Wang, "Using Statically Computed Invariants inside the Predicate Abstraction and Refinement Loop," in Proceeding of CAV, 2006.

Digital Library

[26]

M. Ganai, A. Mukaiyama, A. Gupta, and K. Wakabayashi, "Another Dimension to High Level Synthesis: Verification," in Proceedings of Workshop on Designing Correct Circuits, 2006.

Cited By

Beyer DChien PLee N(2024)Augmenting Interpolation-Based Model Checking with Auxiliary InvariantsModel Checking Software10.1007/978-3-031-66149-5_13(227-247)Online publication date: 10-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-66149-5_13
Riener HHaedicke FFrehse SSoeken MGroβe DDrechsler RFey G(2017)metaSMTInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0426-119:5(605-621)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10009-016-0426-1
Collavizza HLe Vinh NPonsini ORueher MRollet A(2014)Constraint-based BMCInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0258-616:1(103-121)Online publication date: 1-Feb-2014
https://dl.acm.org/doi/10.1007/s10009-012-0258-6
Show More Cited By

Index Terms

Accelerating high-level bounded model checking
1. Hardware

Recommendations

Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Bounded model checking of high-integrity software
HILT '13

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Evaluation of SAT-based Bounded Model Checking of ACTL Properties
TASE '07: Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering

Bounded model checking (BMC) based on SAT has been introduced as a complementary method to BDDbased symbolic model checking of LTL and ACTL properties in recent years. For general LTL and ACTL properties, BMC has traditionally aimed mainly at error ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

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

November 2006

147 pages

ISBN:1595933891

DOI:10.1145/1233501

General Chair:
Soha Hassoun
Tufts Univ., Medford, MA

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CAS: Circuits & Systems
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 November 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ICCAD06

Sponsor:

SIGDA
IEEE-CAS
IEEE-CS

ICCAD06: The International Conference on Computer-Aided Design 2006

November 5 - 9, 2006

California, San Jose

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
318
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Beyer DChien PLee N(2024)Augmenting Interpolation-Based Model Checking with Auxiliary InvariantsModel Checking Software10.1007/978-3-031-66149-5_13(227-247)Online publication date: 10-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-66149-5_13
Riener HHaedicke FFrehse SSoeken MGroβe DDrechsler RFey G(2017)metaSMTInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0426-119:5(605-621)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10009-016-0426-1
Collavizza HLe Vinh NPonsini ORueher MRollet A(2014)Constraint-based BMCInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0258-616:1(103-121)Online publication date: 1-Feb-2014
https://dl.acm.org/doi/10.1007/s10009-012-0258-6
Liu LVasudevan SAyala JJones AMadden PCoskun A(2013)Scaling RTL property checking using feasible path analysisand decompositionProceedings of the 23rd ACM international conference on Great lakes symposium on VLSI10.1145/2483028.2483086(173-178)Online publication date: 2-May-2013
https://dl.acm.org/doi/10.1145/2483028.2483086
Zhang YLi HLi X(2013)Automatic Test Program Generation Using Executing-Trace-Based Constraint Extraction for Embedded ProcessorsIEEE Transactions on Very Large Scale Integration (VLSI) Systems10.1109/TVLSI.2012.220813021:7(1220-1233)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1109/TVLSI.2012.2208130
Ramalho MFreitas MSousa FMarques HCordeiro LFischer B(2013)SMT-Based Bounded Model Checking of C++ ProgramsProceedings of the 20th Annual IEEE International Conference and Workshops on the Engineering of Computer Based Systems10.1109/ECBS.2013.15(147-156)Online publication date: 22-Apr-2013
https://dl.acm.org/doi/10.1109/ECBS.2013.15
Liu LKong WAndo TYatsu HFukuda A(2013)A Survey of Acceleration Techniques for SMT-Based Bounded Model CheckingProceedings of the 2013 International Conference on Computer Sciences and Applications10.1109/CSA.2013.135(554-559)Online publication date: 14-Dec-2013
https://dl.acm.org/doi/10.1109/CSA.2013.135
Belaid MMichel CRueher M(2012)Boosting Local Consistency Algorithms over Floating-Point NumbersProceedings of the 18th International Conference on Principles and Practice of Constraint Programming - Volume 751410.5555/2969951.2969968(127-140)Online publication date: 8-Oct-2012
https://dl.acm.org/doi/10.5555/2969951.2969968
Liu TNagel MTaghdiri M(2012)Bounded Program Verification Using an SMT SolverProceedings of the 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation10.1109/ICST.2012.90(101-110)Online publication date: 17-Apr-2012
https://dl.acm.org/doi/10.1109/ICST.2012.90
Cordeiro LFischer BTaylor RGall HMedvidović N(2011)Verifying multi-threaded software using smt-based context-bounded model checkingProceedings of the 33rd International Conference on Software Engineering10.1145/1985793.1985839(331-340)Online publication date: 21-May-2011
https://dl.acm.org/doi/10.1145/1985793.1985839
Show More Cited By

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