[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/1065579.1065773acmconferencesArticle/Chapter ViewAbstractPublication PagesdacConference Proceedingsconference-collections
Article

Beyond safety: customized SAT-based model checking

Published: 13 June 2005 Publication History

Abstract

Model checking of safety properties has taken a significant lead over non-safety properties in recent years. To bridge the gap, we propose dedicated SAT-based model checking algorithms for properties beyond safety. Previous bounded model checking (BMC) approaches have relied on either converting such properties to safety checking, or finding proofs by deriving termination criteria using loop-free path analysis. Instead, our approach uses a customized SAT-based formulation for bounded model checking of non-safety properties, and determines the completeness bounds for liveness using unbounded SAT-based analysis. Our main contributions are: 1) Customized property translations for LTL formulas for BMC, with novel features that utilize partitioning, learning, and incremental formulation. Customized translations not only improve the BMC performance significantly in comparison to standard monolithic LTL translations, but also allow efficient derivation and use of completeness bounds. Though we discuss the translation schemas for liveness, they can be easily extended to handle other LTL properties as well. 2) Customized formulations for determining completeness bounds for liveness using SAT-based unbounded model checking (UMC) rather than using loop-free path analysis. These formulations comprise greatest fixed-point and least fixed-point computations to efficiently handle nested properties using SAT-based quantification approaches. We show the effectiveness of our overall approach for checking liveness on public benchmarks and several industry designs.

References

[1]
B. Alpern and F. B. Schneider, "Defining liveness," Information Processing Letters, 1985.]]
[2]
A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs," in Proceedings of TACAS, 1999.]]
[3]
A. Cimatti, M. Pistore, M. Roveri, and R. Sebastiani, "Improving the Encoding of LTL Model Checking into SAT," Proceedings of VMCAI, 2002.]]
[4]
M. Sheeran, S. Singh, and G. Stalmarck, "Checking Safety Properties using Induction and a SAT Solver," in Proceedings of FMCAD, 2000.]]
[5]
A. Gupta, M. Ganai, C. Wang, Z. Yang, and P. Ashar, "Abstraction and Bdds Complement SAT-Based BMC in DiVer," in Proceedings of CAV, 2003.]]
[6]
A. Gupta, Z. Yang, P. Ashar, and A. Gupta, "SAT-based Image Computation with Application in Reachability Analysis," in Proceedings of FMCAD, 2000.]]
[7]
K. McMillan, "Applying SAT methods in Unbounded Symbolic Model Checking," in Proceedings of CAV, 2002.]]
[8]
K. McMillan, "Interpolation and SAT-based Model Checking," in Proceedings of CAV, 2003.]]
[9]
M. Ganai, A. Gupta, and P. Ashar, "Efficient SAT-based Symbolic Unbounded Model Checking Using Circuit Cofactoring," in Proceedings of ICCAD, 2004.]]
[10]
K. McMillan and N. Amla, "Automatic Abstraction without Counterexamples," in Proceedings of TACAS, 2003.]]
[11]
A. Gupta, M. Ganai, P. Ashar, and Z. Yang, "Iterative Abstraction using SAT-based BMC with Proof Analysis," in Proceedings of ICCAD, 2003.]]
[12]
E. M. Clarke, O. Grumberg, and D. Peled, Model Checking: MIT Press, 1999.]]
[13]
K. L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem: Kluwer Academic Publishers, 1993.]]
[14]
"Liveness Manifesto. Beyond Safety International Workshop. 2004."]]
[15]
P. Wolper, M. Y. Vardi, and A. P. Sistla, "Reasoning about infinite computation paths.," Proceedings of Symposium on FCS, 1983.]]
[16]
R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper, "Simple on-the-fly automatic verification of linear temporal logic," Protocol Specification, Testing and Verification, 1995.]]
[17]
M. Daniele, F. Giunchiglia, and M. Y. Vardi, "Improved automata generation for linear time temporal logic," Proceedings of CAV, 1999.]]
[18]
F. Somenzi and R. Bloem, "Efficient Buchi Automata from LTL formulae," Proceedings of CAV, 2000.]]
[19]
D. Kroening and O. Shtrichman, "Efficient computation of recurrence diameter," Proceedings of VMCAI, 2003.]]
[20]
A. Biere, C. Artho, and V. Schuppan, "Liveness Checking as Safety Checking," Proceedings of FMICS, 2002.]]
[21]
M. Awedh and F. Somenzi, "Proving more properties with Bounded Model Checking," Proceedings of CAV, 2004.]]
[22]
O. Shtrichman, "Pruning Techniques for the SAT-based bounded model checking," in Proceedings of TACAS, 2001.]]
[23]
J. Whittemore, J. Kim, and K. Sakallah, "SATIRE: A New Incremental Satisfiability Engine," Proceedings of DAC, 2001.]]
[24]
M. Ganai and A. Aziz, "Improved SAT-based Bounded Reachability Analysis," in Proceedings of VLSI Design Conference, 2002.]]
[25]
M. Ganai, L. Zhang, P. Ashar, and A. Gupta, "Combining Strengths of Circuit-based and CNF-based Algorithms for a High Performance SAT Solver," in Proceedings of DAC, 2002.]]
[26]
"The VIS Home Page. http://www-cad.eecs.berkeley.edu/Respep/Research/vis/."]]
[27]
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver," in Proceedings of DAC, 2001.]]
[28]
M. Ganai, A. Gupta, and P. Ashar, "DiVer: SAT-based Model Checking Platform for Verifying Large Scale Systems", in Proceedings of TACAS, 2005.]]

Cited By

View all
  • (2011)Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based LanguagesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.68.568(39-53)Online publication date: 12-Sep-2011
  • (2010)SAT-based semiformal verification of hardwareProceedings of the 2010 Conference on Formal Methods in Computer-Aided Design10.5555/1998496.1998505(25-32)Online publication date: 20-Oct-2010
  • (2010)Hardware-VerifikationDigitale Hardware/Software-Systeme10.1007/978-3-642-05356-6_6(235-359)Online publication date: 20-May-2010
  • Show More Cited By

Index Terms

  1. Beyond safety: customized SAT-based model checking

    Recommendations

    Comments

    Please enable JavaScript to view thecomments powered by Disqus.

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    DAC '05: Proceedings of the 42nd annual Design Automation Conference
    June 2005
    984 pages
    ISBN:1595930582
    DOI:10.1145/1065579
    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

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 13 June 2005

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. LTL
    2. SAT
    3. bounded model checking
    4. circuit cofactoring
    5. formal verification
    6. liveness
    7. unbounded model checking

    Qualifiers

    • Article

    Conference

    DAC05
    Sponsor:
    DAC05: The 42nd Annual Design Automation Conference 2005
    June 13 - 17, 2005
    California, Anaheim, USA

    Acceptance Rates

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

    Upcoming Conference

    DAC '25
    62nd ACM/IEEE Design Automation Conference
    June 22 - 26, 2025
    San Francisco , CA , USA

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)4
    • Downloads (Last 6 weeks)2
    Reflects downloads up to 04 Jan 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2011)Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based LanguagesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.68.568(39-53)Online publication date: 12-Sep-2011
    • (2010)SAT-based semiformal verification of hardwareProceedings of the 2010 Conference on Formal Methods in Computer-Aided Design10.5555/1998496.1998505(25-32)Online publication date: 20-Oct-2010
    • (2010)Hardware-VerifikationDigitale Hardware/Software-Systeme10.1007/978-3-642-05356-6_6(235-359)Online publication date: 20-May-2010
    • (2008)Tunneling and slicingProceedings of the 45th annual Design Automation Conference10.1145/1391469.1391507(137-142)Online publication date: 8-Jun-2008
    • (2007)Efficient BMC for Multi-Clock Systems with Clocked Specifications2007 Asia and South Pacific Design Automation Conference10.1109/ASPDAC.2007.358004(310-315)Online publication date: Jan-2007
    • (2006)Accelerating high-level bounded model checkingProceedings of the 2006 IEEE/ACM international conference on Computer-aided design10.1145/1233501.1233664(794-801)Online publication date: 5-Nov-2006
    • (2006)Accelerating High-level Bounded Model Checking2006 IEEE/ACM International Conference on Computer Aided Design10.1109/ICCAD.2006.320122(794-801)Online publication date: Nov-2006
    • (2006)SAT-Based verification methods and applications in hardware verificationProceedings of the 6th international conference on Formal Methods for the Design of Computer, Communication, and Software Systems10.1007/11757283_5(108-143)Online publication date: 22-May-2006

    View Options

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Media

    Figures

    Other

    Tables

    Share

    Share

    Share this Publication link

    Share on social media