Property Directed Abstract Interpretation | SpringerLink
Skip to main content
Springer Nature Link
Log in

Property Directed Abstract Interpretation

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)

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

  • 1196 Accesses

Abstract

Recently, Bradley proposed the PDR/IC3 model checking algorithm for verifying safety properties, where forward and backward reachability analyses are intertwined, and guide each other. Many variants of Bradley’s original algorithm have been developed and successfully applied to both hardware and software verification. However, these algorithms have been presented in an operational manner, in disconnect with the rich literature concerning the theoretical foundation of static analysis formulated by abstract interpretation.

Inspired by PDR, we develop a nonstandard semantics which computes for every \(0 \le N\) an over-approximation of the set of traces of length N leading to a safety violation. The over approximation is precise, in the sense that it only includes traces that do not start at an initial state, unless the program is unsafe, and in this case the semantics aborts at a special error state. In a way, the semantics computes multiple over-approximations of bounded unsafe program behaviors using a sequence of abstractions whose precision grows automatically with N.

We show that existing PDR algorithms can be described as a specific implementation of our semantics, performing an abstract interpretation of the program, but instead of aiming for a fixpoint, they stop early when either the backward analysis finds a counterexample or the states comprising one of the bounded traces provides sufficient evidence that the program is safe. This places PDR within the solid framework of abstract interpretation, and thus provides a unified explanation of the different PDR algorithms as well as a new proof of their soundness.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    In this paper, we focus on linear property directed reachability, as opposed to, e.g., tree-IC3 [5]. See Sect. 9.

  2. 2.

    In model checking nomenclature, the abstraction of \(\omega _N(i)\) into \(\omega ^{\sharp }_N(i)\) is called generalization.

References

  1. Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 831–848. Springer, Heidelberg (2014)

    Google Scholar 

  2. Bjørner, N., Gurfinkel, A.: Property directed polyhedral abstraction. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 263–281. Springer, Heidelberg (2015)

    Google Scholar 

  3. Bradley, A.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 6538, pp. 70–78. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Chockler, H., Ivrii, A., Matsliah, A., Moran, S., Nevo, Z.: Incremental formal verification of hardware. In: International Conference on Formal Methods in Computer-Aided Design - FMCAD, pp. 135–143 (2011)

    Google Scholar 

  5. Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E., (ed.) Formal Descriptions of Programming Concepts, (IFIP WG 2.2, St. Andrews, Canada, August 1977), pp. 237–277. North-Holland (1978)

    Google Scholar 

  7. Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, pp. 125–134 (2011)

    Google Scholar 

  8. Gurfinkel, A.: IC3, PDR and friends. http://arieg.bitbucket.org/pdf/gurfinkel_ssft15.pdf

  9. Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  10. Karbyshev, A., Bjørner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 583–602. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

Download references

Acknowledgments

We thank Mooly Sagiv, Eran Yahav, and the anonymous referees for their helpful comments. This work was supported by the European Research Council under the European Union’s Seventh Framework Program (FP7/2007-2013) / ERC grant agreement no. [321174-VSSC], EU FP7 project ADVENT (308830), by Broadcom Foundation and Tel Aviv University Authentication Initiative, and by BSF grant no. 2012259.

Author information

Authors and Affiliations

  1. Tel Aviv University, Tel Aviv, Israel

    Noam Rinetzky

  2. The Academic College of Tel Aviv Yaffo, Tel Aviv, Israel

    Sharon Shoham

Authors
  1. Noam Rinetzky
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sharon Shoham
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sharon Shoham .

Editor information

Editors and Affiliations

  1. EPFL IC-DO, Lausanne, Switzerland

    Barbara Jobstmann

  2. Microsoft Research, Redmond, Washington, USA

    K. Rustan M. Leino

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rinetzky, N., Shoham, S. (2016). Property Directed Abstract Interpretation. In: Jobstmann, B., Leino, K. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2016. Lecture Notes in Computer Science(), vol 9583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49122-5_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-49122-5_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-49121-8

  • Online ISBN: 978-3-662-49122-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation