Skip to main content
SpringerLink
Log in

Viper: A Verification Infrastructure for Permission-Based Reasoning

  • 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))

Abstract

The automation of verification techniques based on first-order logic specifications has benefitted greatly from verification infrastructures such as Boogie and Why. These offer an intermediate language that can express diverse language features and verification techniques, as well as back-end tools: in particular, verification condition generators.

However, these infrastructures are not well suited to verification techniques based on separation logic and other permission logics, because they do not provide direct support for permissions and because existing tools for these logics often favour symbolic execution over verification condition generation. Consequently, tool support for these logics (where available) is typically developed independently for each technique, dramatically increasing the burden of developing automatic tools for permission-based verification.

In this paper, we present a verification infrastructure whose intermediate language supports an expressive permission model natively. We provide tool support including two back-end verifiers: one based on symbolic execution, and one on verification condition generation; an inference tool based on abstract interpretion is currently under development. A wide range of existing verification techniques can be implemented via this infrastructure, alleviating much of the burden of building permission-based verifiers, and allowing the developers of higher-level reasoning techniques to focus their efforts at an appropriate level of abstraction.

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 EPUB and 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

References

  1. Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54(6), 81–91 (2011)

    Article  Google Scholar 

  2. Bengtson, J., Jensen, J.B., Birkedal, L.: A framework for higher-order separation logic in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 315–331. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 202–217. Springer, Heidelberg (2015)

    Google Scholar 

  5. Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127–131. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  6. Botincan, M., Distefano, D., Dodds, M., Grigore, R., Naudziuniene, D., Parkinson, M.J.: coreStar: the core of jStar. In: Leino, K.R.M., Moskal, M. (eds.) BOOGIE 2011, pp. 65–77 (2011). http://research.microsoft.com/en-us/um/people/moskal/boogie2011/boogie_2011_all.pdf

  7. Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Boyland, J.T., Müller, P., Schwerhoff, M., Summers, A.J.: Constraint semantics for abstract read permissions. In: FTfJP 2014, pp. 2:1–2:6. ACM, New York, NY, USA (2014)

    Google Scholar 

  9. Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006–1036 (2012)

    Article  MATH  Google Scholar 

  10. Chlipala, A., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: Hutton, G., Tolmach, A.P. (eds.) ICFP, pp. 79–90. ACM (2009)

    Google Scholar 

  11. Cohen, E., Moskal, M., Schulte, W., Tobies, S.: Local verification of global invariants in concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 480–494. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Dockins, R., Hobor, A., Appel, A.W.: A fresh look at separation algebras and share accounting. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 161–177. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  13. Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. Heule, S., Kassios, I.T., Müller, P., Summers, A.J.: Verification condition generation for permission logics with abstract predicates and abstraction functions. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 451–476. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  16. Heule, S., Leino, K.R.M., Müller, P., Summers, A.J.: Abstract read permissions: fractional permissions without the fractions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 315–334. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  17. Hoare, C.A.R.: Proof of correctness of data representation. Acta Informatica 1(4), 271–281 (1972)

    Article  MATH  Google Scholar 

  18. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573–609 (2015)

    Article  MathSciNet  Google Scholar 

  20. Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427–443. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  21. Leavens, G., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kilov, I., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer, Dordrecht (1999)

    Chapter  Google Scholar 

  22. Leino, K.R.M.: This is Boogie 2. Working draft (2008). http://research.microsoft.com/en-us/um/people/leino/papers.html

  23. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  24. Leino, K.R.M., Müller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378–393. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  25. Leino, K.R.M., Müller, P.: Using the Spec# language, methodology, and tools to write bug-free programs. In: Müller, P. (ed.) LASER Summer School 2007/2008. LNCS, vol. 6029, pp. 91–139. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  26. Leino, K.R.M., Müller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD. LNCS, vol. 5705, pp. 195–222. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  27. Moskal, M.: Programming with triggers. In: SMT 2009, pp. 20–29. ACM, New York, NY, USA (2009)

    Google Scholar 

  28. Müller, P., Schwerhoff, M., Summers, A.J.: Online appendix. http://viper.ethz.ch/VMCAI16

  29. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  30. Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL, pp. 247–258 (2005)

    Google Scholar 

  31. Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. Logical Methods Comput. Sci. 8(3:01), 1–54 (2012)

    MathSciNet  Google Scholar 

  32. Navarro Pérez, J.A., Rybalchenko, A.: Separation logic modulo theories. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 90–106. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  33. Piskac, R., Wies, T., Zufferey, D.: GRASShopper—complete heap verification with mixed specifications. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 124–139. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  34. Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)

    Google Scholar 

  35. Schwerhoff, M., Summers, A.J.: Lightweight support for magic wands in an automatic verifier. In: Boyland, J.T. (ed.) ECOOP, vol. 37 of LIPIcs, pp. 614–638. Schloss Dagstuhl (2015)

    Google Scholar 

  36. Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 148–172. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  37. Tuerk, T.: A formalisation of Smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469–484. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Acknowledgements

This work has been funded in part by the Swiss National Science Foundation and by the Hasler Foundation. Viper has benefitted from the work of many people. We are especially grateful to Uri Juhasz for his contributions to the design of the Viper language, Ioannis Kassios for his work on quantified permissions and the initial Chalice front-end, and to Vytautas Astrauskas for his improvements of the latter. We are also thankful to Milos Novacek for his work on specification inference, and to Stefan Heule for the initial development of the verification condition generator. We warmly thank Stefan Blom for his extensive feedback on Viper and his help with using VerCors, and Marco Eilers for his help with our experimental evaluation.

Author information

Authors and Affiliations

  1. Department of Computer Science, ETH Zurich, Zurich, Switzerland

    Peter Müller, Malte Schwerhoff & Alexander J. Summers

Authors
  1. Peter Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Malte Schwerhoff
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexander J. Summers
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Müller .

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

Müller, P., Schwerhoff, M., Summers, A.J. (2016). Viper: A Verification Infrastructure for Permission-Based Reasoning. 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_2

Download citation

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

  • 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