Skip to main content
SpringerLink
Log in
Book cover

Aliasing in Object-Oriented Programming. Types, Analysis and Verification pp 407–442Cite as

VeriFast for Java: A Tutorial

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7850))

Abstract

VeriFast is a separation logic-based program verifier for Java. This tutorial introduces the verifier’s features step by step.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Parkinson, M., Bierman, G.: Separation Logic for Object-Oriented Programming. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. LNCS, vol. 7850, pp. 366–406. Springer, Heidelberg (2013)

    Google Scholar 

  2. Jacobs, B., Smans, J., Piessens, F.: A Quick Tour of the VeriFast Program Verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304–311. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  3. Jacobs, B., Smans, J., Piessens, F.: The VeriFast Program Verifier: A Tutorial (2012)

    Google Scholar 

  4. Jacobs, B., Smans, J., Piessens, F.: Verification of imperative programs: The VeriFast approach. a draft course text. Technical Report CW578, Department of Computer Science, K.U.Leuven (2010)

    Google Scholar 

  5. Gosling, J., Joy, B., Steele, G., Bracha, G., Buckley, A.: The Java Language Specification (2012)

    Google Scholar 

  6. Meyer, B.: Applying “Design by Contract”. IEEE Computer 25(10) (1992)

    Google Scholar 

  7. de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. 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 

  9. Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Symposium on Principles of Programming Languages (POPL). ACM (2005)

    Google Scholar 

  10. Parkinson, M.: Class invariants: The end of the road? In: International Workshop on Aliasing, Confinement and Ownership in Object-oriented Programming, IWACO (2007)

    Google Scholar 

  11. Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Symposium on Principles of Programming Languages (POPL). ACM (2008)

    Google Scholar 

  12. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6) (2003)

    Google Scholar 

  13. O’Hearn, P., Reynolds, J., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Google Scholar 

  14. Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Symposium on Logic in Computer Science, LICS (2002)

    Google Scholar 

  15. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10) (1969)

    Google Scholar 

  16. Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  17. Distefano, D., Parkinson, M.: jStar: Towards practical verification for Java. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM (2008)

    Google Scholar 

  18. Villard, J., Lozes, É., Calcagno, C.: Proving Copyless Message Passing. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 194–209. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated Verification of Shape and Size Properties Via Separation Logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  20. 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 

  21. Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Reasoning with the awkward squad. In: International Conference on Functional Programming (ICFP). ACM (2008)

    Google Scholar 

  22. Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle Semantics for Concurrent Separation Logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 353–367. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  23. Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Symposium on Principles of Programming Languages (POPL). ACM (2007)

    Google Scholar 

  24. Kassios, I.T.: Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  25. Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional Logic for Local Reasoning about Global Invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 387–411. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  26. Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM (1998)

    Google Scholar 

  27. 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 

  28. Dietl, W.M.: Universe Types: Topology, Encapsulation, Genericity, and Tools. PhD thesis, ETH Zurich, Switzerland (2009)

    Google Scholar 

  29. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  30. Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Communications of the ACM 54(6) (2011)

    Google Scholar 

  31. 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 

  32. Smans, J., Jacobs, B., Piessens, F., Schulte, W.: An Automatic Verifier for Java-Like Programs Based on Dynamic Frames. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 261–275. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  33. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI). ACM (2002)

    Google Scholar 

  34. Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contract-based modular verification of concurrent C. In: International Conference on Software Engineering (ICSE). IEEE (2009)

    Google Scholar 

  35. Jacobs, B., Piessens, F., Smans, J., Leino, K.R.M., Schulte, W.: A programming model for concurrent object-oriented programs. ACM Transactions on Programming Languages and Systems 31(1) (2008)

    Google Scholar 

  36. Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Transactions on Programming Languages and Systems 34(1) (2012)

    Google Scholar 

  37. Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM 19(5) (1976)

    Google Scholar 

  38. Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: Symposium on Principles of Programming Languages (POPL). ACM (2011)

    Google Scholar 

  39. Jacobs, B., Piessens, F.: Dynamic owicki-gries reasoning using ghost fields and fractional permissions. Technical Report CW549, Department of Computer Science, K.U.Leuven (2009)

    Google Scholar 

  40. Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent Abstract Predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  41. Krishnaswami, N.R., Turon, A., Dreyer, D., Garg, D.: Superficially substructural types. In: International Conference on Functional Programming (ICFP). ACM (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. iMinds-DistriNet, KU Leuven, Belgium

    Jan Smans, Bart Jacobs & Frank Piessens

Authors
  1. Jan Smans
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bart Jacobs
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Frank Piessens
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Katholieke Universiteit Leuven, Celestijnenlaan 200A, 3001, Heverlee, Belgium

    Dave Clarke

  2. School of Engineering and Computer Science, Victoria University of Wellington, Cottn Building, Gate 6, Kelburn Parade, 6140, Wellington, New Zealand

    James Noble

  3. Department of Information Technology, Uppsala University, Lägerhyddsvägen 2, 75237, Uppsala, Sweden

    Tobias Wrigstad

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Smans, J., Jacobs, B., Piessens, F. (2013). VeriFast for Java: A Tutorial. In: Clarke, D., Noble, J., Wrigstad, T. (eds) Aliasing in Object-Oriented Programming. Types, Analysis and Verification. Lecture Notes in Computer Science, vol 7850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36946-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-36946-9_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-36945-2

  • Online ISBN: 978-3-642-36946-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation