Skip to main content
SpringerLink
Log in

Understanding IC3

  • Conference paper
Theory and Applications of Satisfiability Testing – SAT 2012 (SAT 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7317))

Abstract

The recently introduced model checking algorithm, IC3, has proved to be among the best SAT-based safety model checkers. Many implementations now exist. This paper provides the context from which IC3 was developed and explains how the originator of the algorithm understands it. Then it draws parallels between IC3 and the subsequently developed algorithms, FAIR and IICTL, which extend IC3’s ideas to the analysis of ω-regular and CTL properties, respectively. Finally, it draws attention to certain challenges that these algorithms pose for the SAT and SMT community.

Work supported in part by the Semiconductor Research Corporation under contract GRC 2271.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Bradley, A.R.: k-step relative inductive generalization. Technical report, CU Boulder (March 2010), http://arxiv.org/abs/1003.3649

  3. Bradley, A.R.: SAT-Based Model Checking without Unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD (November 2007)

    Google Scholar 

  5. Bradley, A.R., Manna, Z.: Verification Constraint Problems with Strengthening. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 35–49. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: FMCAD (November 2011)

    Google Scholar 

  7. Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear Invariant Generation Using Non-linear Constraint Solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)

    Google Scholar 

  9. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL (January 1978)

    Google Scholar 

  10. Graf, S., Saidi, H.: Construction of Abstract state Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 73–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  11. Hassan, Z., Bradley, A.R., Somenzi, F.: Incremental, inductive CTL model checking. In: CAV (July 2012)

    Google Scholar 

  12. Lu, F., Iyer, M.K., Parthasarathy, G., Wang, L.-C., Cheng, K.-T., Chen, K.C.: An Efficient Sequential SAT Solver With Improved Search Strategies. In: DATE (2005)

    Google Scholar 

  13. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)

    Book  Google Scholar 

  14. McMillan, K.L.: Applying SAT Methods in Unbounded Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250–264. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  16. McMillan, K.L.: Symbolic Model Checking. Kluwer, Boston (1994)

    Google Scholar 

  17. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable Analysis of Linear Systems Using Mathematical Programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Sheeran, M., Singh, S., Stålmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Somenzi, F., Bradley, A.R.: IC3: Where monolithic and incremental meet. In: FMCAD (November 2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ECEE Department, University of Colorado at Boulder, USA

    Aaron R. Bradley

Authors
  1. Aaron R. Bradley
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Center for Information Technology, Fondazione Bruno Kessler, via Sommarive 18, Povo, 38123, Trento, Italy

    Alessandro Cimatti

  2. Department of Information Engineering and Computer Science, University of Trento, via Sommarive 14, Povo, 38123, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bradley, A.R. (2012). Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds) Theory and Applications of Satisfiability Testing – SAT 2012. SAT 2012. Lecture Notes in Computer Science, vol 7317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31612-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31612-8_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31611-1

  • Online ISBN: 978-3-642-31612-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation