Skip to main content
SpringerLink
Log in
Book cover

LASER Summer School on Software Engineering

LASER 2011: Tools for Practical Software Verification pp 133–155Cite as

Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach

  • Chapter

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

Abstract

Static program verifiers such as Spec#, Dafny, jStar, and VeriFast define the state of the art in automated functional verification techniques. The next open challenges are to make verification tools usable even by programmers not fluent in formal techniques. This paper discusses some techniques used in AutoProof, a verification tool that translates Eiffel programs to Boogie and uses the Boogie verifier to prove them. In an effort to be usable with real programs, AutoProof fully supports several advanced object-oriented features including polymorphism, inheritance, and function objects. AutoProof also adopts simple strategies to reduce the amount of annotations needed when verifying programs (e.g., frame conditions). The paper illustrates the main features of AutoProof’s translation, including some whose implementation is underway, and demonstrates them with examples and a case study.

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   49.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. Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional Logic for Local Reasoning about Global Invariants. In: Dell’Acqua, P. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 387–411. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Darvas, Á., Leino, K.R.M.: Practical Reasoning About Invocations and Implementations of Pure Methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, pp. 336–351. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Distefano, D., Parkinson, M.J.: jStar: Towards Practical Verification for Java. In: Proceedings of OOPSLA, pp. 213–226 (2008)

    Google Scholar 

  5. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234–245. ACM (2002)

    Google Scholar 

  6. Furia, C.A., Meyer, B.: Inferring Loop Invariants Using Postconditions. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol. 6300, pp. 277–300. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison Wesley (1994)

    Google Scholar 

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

  9. Leavens, G.T., Leino, K.R.M., Müller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing 19(2), 159–189 (2007)

    Article  MATH  Google Scholar 

  10. Leino, K.R.M.: This is Boogie 2. Technical report, Microsoft Research (2008)

    Google Scholar 

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

  12. Leino, K.R.M., Müller, P.: Verification of Equivalent-Results Methods. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 307–321. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

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

  14. Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall (1997)

    Google Scholar 

  15. Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  16. Müller, P., Nordio, M.: Proof-transforming compilation of programs with abrupt termination. In: SAVCBS 2007: Proceedings of the 2007 Conference on Specification and Verification of Component-Based Systems, pp. 39–46 (2007)

    Google Scholar 

  17. Nordio, M.: Proofs and Proof Transformations for Object-Oriented Programs. PhD thesis, ETH Zurich, Switzerland (2009)

    Google Scholar 

  18. Nordio, M., Calcagno, C., Meyer, B., Müller, P.: Reasoning about Function Objects. Technical Report 615, ETH Zurich (2008)

    Google Scholar 

  19. Nordio, M., Calcagno, C., Meyer, B., Müller, P., Tschannen, J.: Reasoning about Function Objects. In: Vitek, J. (ed.) TOOLS 2010. LNCS, vol. 6141, pp. 79–96. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  20. Nordio, M., Calcagno, C., Müller, P., Meyer, B.: A Sound and Complete Program Logic for Eiffel. In: Oriol, M., Meyer, B. (eds.) TOOLS EUROPE 2009. LNBIP, vol. 33, pp. 195–214. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  21. Nordio, M., Estler, H.-C., Furia, C.A., Meyer, B.: Collaborative software development on the web, arXiv:1105.0768v3 (2011)

    Google Scholar 

  22. Nordio, M., Müller, P., Meyer, B.: Proof-Transforming Compilation of Eiffel Programs. In: Paige, R.F., Meyer, B. (eds.) TOOLS-EUROPE 2008. LNBIP, vol. 11, pp. 316–335. Springer, Heidelberg (2008)

    Google Scholar 

  23. O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004, pp. 268–280 (2004)

    Google Scholar 

  24. Polikarpova, N., Furia, C.A., Meyer, B.: Specifying Reusable Components. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 127–141. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  25. Tschannen, J.: Automatic verification of Eiffel programs. Master’s thesis, Chair of Software Engineering, ETH Zurich (2009)

    Google Scholar 

  26. Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 382–398. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  27. Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Verifying Eiffel programs with Boogie. In: First International Workshop on Intermediate Verification Languages, BOOGIE (2011), http://arxiv.org/abs/1106.4700

  28. van Staden, S., Calcagno, C., Meyer, B.: Verifying Executable Object-Oriented Specifications with Separation Logic. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 151–174. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Chair of Software Engineering, ETH Zurich, Switzerland

    Julian Tschannen, Carlo Alberto Furia, Martin Nordio & Bertrand Meyer

Authors
  1. Julian Tschannen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carlo Alberto Furia
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin Nordio
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Bertrand Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. ETH Zurich, Clausiusstrasse 59, 8092, Zurich, Switzerland

    Bertrand Meyer  & Martin Nordio  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Tschannen, J., Furia, C.A., Nordio, M., Meyer, B. (2012). Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach. In: Meyer, B., Nordio, M. (eds) Tools for Practical Software Verification. LASER 2011. Lecture Notes in Computer Science, vol 7682. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35746-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-35746-6_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-35745-9

  • Online ISBN: 978-3-642-35746-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation