research-article

Tunneling and slicing: towards scalable BMC

Authors:

Aarti GuptaAuthors Info & Claims

DAC '08: Proceedings of the 45th annual Design Automation Conference

Pages 137 - 142

https://doi.org/10.1145/1391469.1391507

Published: 08 June 2008 Publication History

Abstract

Bounded Model Checking (BMC) provides complete design coverage with respect to a correctness property up to a bounded depth. However, with successive unrolling of the design, each BMC instance at depth k becomes bigger in size and harder to solve. We propose a novel scalable approach to decompose disjunctively a BMC instance, into simpler and independent subproblems, based on tunnels i.e., a set of control paths. We simplify each subproblem using slicing, data path simplification and tunnel specific control flow constraints, and solve them independently. We implemented such a tunneling and slicing-based reduction (TSR) approach in Satisfiability-Modulo-Theory (SMT)-based BMC framework. Such a TSR-based approach improves the overall performance of BMC when applied to verification of lowlevel embedded industry programs.

References

[1]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS, 1999.]]

Digital Library

[2]

A. Armando, J. Mantovani, and L. Platania. Bounded model checking of software using SMT solvers instead of SAT solvers. In Proc. of SPIN Workshop, 2006.]]

Digital Library

[3]

Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.]]

Digital Library

[4]

M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. V. Rossum, M. Schulz, and R. Sebastiani. The MathSAT 3 System. In Proc. of CADE, 2005.]]

Digital Library

[5]

R. Nieuwenhuis and A. Oliveras. DPLL(T) with exhaustive theory propogation and its application to difference logic. In Proc. of CAV, 2005.]]

Digital Library

[6]

B. Dutertre and L. de Moura. A fast linear-arithmetic solver for DPLL(T). In Proc. of CAV, 2006.]]

Digital Library

[7]

M. K. Ganai and A. Gupta. Accelerating high-level bounded model checking. In Proc. of ICCAD, 2006.]]

Digital Library

[8]

M. K. Ganai and A. Gupta. SAT-based Scalable Formal Verification Solutions. Springer Science and Business Media, 2007.]]

Digital Library

[9]

M. K. Ganai, A. Gupta, Z. Yang, and P. Ashar. Efficient distributed SAT and SAT-based distributed bounded model checking. Journal on STTT, 8(4--5): 387--396, 2006.]]

[10]

M. K. Ganai, A. Gupta, and P. Ashar. Beyond safety: Customized SAT-based model checking. In Proc. of DAC, 2005.]]

Digital Library

[11]

A. Narayan, A. J. Isles, J. Jain, R. K. Brayton, and A. Sangiovanni-Vincentelli. Reachability analysis using partitioned-ROBDDs. In Proc. of ICCAD, 1997.]]

Digital Library

[12]

T. Heyman, D. Geist, O. Grumberg, and A. Schuster. Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. In Proc. of CAV, 2000.]]

Digital Library

[13]

S. Barner and I. Rabinovitz. Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning. In Proceedings of CHARME, 2003.]]

[14]

X. Feng, A. Hu, and J. Yang. Partitioned model checking from software specifications. In Proc. of ASPDAC, 2005.]]

Digital Library

[15]

C. Wang, Z. Yang, F. Ivančić, and A. Gupta. Disjunctive image computation for embedded software verification. In Proc. of DATE, 2006.]]

Digital Library

[16]

D. Ward and F. Somenzi. Decomposing image computation for symbolic reachability analysis using control flow information. In Proc. of ICCAD, 2006.]]

Digital Library

[17]

S. Anand, C. Pasareanu, and W. Visser. JPF-SE: A symbolic execution extension to java pathfinder. In Proc. of TACAS, pages 58--70, 2007.]]

Digital Library

[18]

T. Arons, E. Elster, S. Ozer, J. Shalev, and E. Singerman. Efficient symbolic simulation of low level software. In Proc. of DATE, 2008.]]

Digital Library

[19]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proc. of POPL, pages 58--70, 2002.]]

Digital Library

[20]

D. Babic and A. Hu. Structural abstraction of software verification conditions. In Proc. of CAV, 2007.]]

Digital Library

[21]

F. Ivančić, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. F-Soft: Software verification platform. In Proc. of CAV, 2005.]]

Digital Library

[22]

M. Dwyer and J. Hatcliff. Slicing software for model construction. In ACM Workshop on Partial Evaluation and Program Manipulation, 1999.]]

[23]

R. Rugina and M. C. Rinard. Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In Proc. of PLDI, 2000.]]

Digital Library

[24]

G. Karypis and V. Kumar. Multilevel k-way hypergraph partitioning. In Proc. Intl. Conf. on VLSI, 2000.]]

[25]

SRI. Yices: An SMT solver, http://fm.csl.sri.com/yices.]]

Cited By

Darke PChimdyalwar B(2023)OLA: Property Directed Outer Loop Abstraction for Efficient Verification of Reactive Systems2023 IEEE International Conference on Software Maintenance and Evolution (ICSME)10.1109/ICSME58846.2023.00056(436-440)Online publication date: 1-Oct-2023
https://doi.org/10.1109/ICSME58846.2023.00056
Kheireddine ARenault EBaarir S(2022)Towards better heuristics for solving bounded model checking problemsConstraints10.1007/s10601-022-09339-828:1(45-66)Online publication date: 27-Dec-2022
https://doi.org/10.1007/s10601-022-09339-8
Candea GGodefroid P(2019)Automated Software Test Generation: Some Challenges, Solutions, and Recent AdvancesComputing and Software Science10.1007/978-3-319-91908-9_24(505-531)Online publication date: 2019
https://doi.org/10.1007/978-3-319-91908-9_24
Show More Cited By

Index Terms

Tunneling and slicing: towards scalable BMC
1. Applied computing
  1. Physical sciences and engineering
    1. Engineering

Recommendations

Bounded Model Checking of Incomplete Networks of Timed Automata
MTV '10: Proceedings of the 2010 11th International Workshop on Microprocessor Test and Verification

Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is called bounded model checking (BMC). In BMC the system is iteratively unfolded and then transformed into a ...
SMT-Based Bounded Model Checking for Real-Time Systems (Short Paper)
QSIC '08: Proceedings of the 2008 The Eighth International Conference on Quality Software

SAT-based bounded model checking has a high complexity in dealing with real-time systems. SMT solvers can generalize SAT solving by adding the ability to handle arithmetic and other decidable theories. With this advantage, if we use SMT in bounded model ...
Verifying verified code
Abstract
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow-up case study that explores the methodology from the perspective of three research ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '08: Proceedings of the 45th annual Design Automation Conference

June 2008

993 pages

ISBN:9781605581156

DOI:10.1145/1391469

General Chair:
Limor Fix
Intel Research Pittsburgh, Pittsburgh, PA

Copyright © 2008 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

The EDA Consortium
IEEE/CASS/CANDE/CEDA
SIGDA: ACM Special Interest Group on Design Automation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 June 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

DAC '08

Sponsor:

SIGDA

DAC '08: The 45th Annual Design Automation Conference 2008

June 8 - 13, 2008

California, Anaheim

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
183
Total Downloads

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

Reflects downloads up to 05 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Darke PChimdyalwar B(2023)OLA: Property Directed Outer Loop Abstraction for Efficient Verification of Reactive Systems2023 IEEE International Conference on Software Maintenance and Evolution (ICSME)10.1109/ICSME58846.2023.00056(436-440)Online publication date: 1-Oct-2023
https://doi.org/10.1109/ICSME58846.2023.00056
Kheireddine ARenault EBaarir S(2022)Towards better heuristics for solving bounded model checking problemsConstraints10.1007/s10601-022-09339-828:1(45-66)Online publication date: 27-Dec-2022
https://doi.org/10.1007/s10601-022-09339-8
Candea GGodefroid P(2019)Automated Software Test Generation: Some Challenges, Solutions, and Recent AdvancesComputing and Software Science10.1007/978-3-319-91908-9_24(505-531)Online publication date: 2019
https://doi.org/10.1007/978-3-319-91908-9_24
Bornholt JTorlak E(2018)Finding code that explodes under symbolic evaluationProceedings of the ACM on Programming Languages10.1145/32765192:OOPSLA(1-26)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276519
Saissi HBokor PSuri N(2015)PBMC: Symbolic Slicing for the Verification of Concurrent ProgramsAutomated Technology for Verification and Analysis10.1007/978-3-319-24953-7_26(344-360)Online publication date: 22-Nov-2015
https://doi.org/10.1007/978-3-319-24953-7_26
Liu LVasudevan S(2014)Scaling Input Stimulus Generation through Hybrid Static and Dynamic Analysis of RTLACM Transactions on Design Automation of Electronic Systems10.1145/267654920:1(1-33)Online publication date: 18-Nov-2014
https://dl.acm.org/doi/10.1145/2676549
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
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
Kong WLiu LAndo TYatsu HHisazumi KFukuda A(2013)Harnessing SMT-Based Bounded Model Checking through Stateless Explicit-State ExplorationProceedings of the 2013 20th Asia-Pacific Software Engineering Conference (APSEC) - Volume 0110.1109/APSEC.2013.55(355-362)Online publication date: 2-Dec-2013
https://dl.acm.org/doi/10.1109/APSEC.2013.55
Kuznetsov VKinder JBucur SCandea G(2012)Efficient state merging in symbolic executionACM SIGPLAN Notices10.1145/2345156.225408847:6(193-204)Online publication date: 11-Jun-2012
https://dl.acm.org/doi/10.1145/2345156.2254088
Show More Cited By

View Options

Get Access

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.

Media

Figures

Other

Tables

View Table of Contents