Skip to main content
SpringerLink
Log in

Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation

(Invited Talk)

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2011)

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

Abstract

CodeContracts provide a language agnostic way to specify and check preconditions, postconditions and object invariants (collectively called contracts [17]). Specifications take the form of calls to static methods of a Contract library [7]. The authoring library is available out-of-the-box to all .NET programmers from υ4.

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. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  2. Barthe, G., Burdy, L., Charles, J., Grégoire, B., Huisman, M., Lanet, J.-L., Pavlova, M., Requet, A.: JACK — A tool for validation of security and behaviour of Java applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 152–174. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 77–101. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM POPL 1977. ACM, New York (1977)

    Google Scholar 

  5. Cousot, P., Cousot, R., Logozzo, F.: Contract precondition inference from intermittent assertions on collections. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 150–168. Springer, Heidelberg (2011)

    Google Scholar 

  6. Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: ACM POPL 2011. ACM Press, New York (2011)

    Google Scholar 

  7. Fähndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: ACM SAC 2010, ACM Press, New York (2010)

    Google Scholar 

  8. Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: ACM OOPSLA 2003, ACM Press, New York (2003)

    Google Scholar 

  9. Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B. (ed.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011)

    Google Scholar 

  10. Ferrara, P., Logozzo, F., Fähndrich, M.: Safer unsafe code in.NET. In: ACM OOPSLA 2008, ACM Press, New York (2008)

    Google Scholar 

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

  12. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: ACM PLDI 2002. ACM Press, New York (2002)

    Google Scholar 

  13. Laviron, V., Logozzo, F.: Refining abstract interpretation-based static analyses with hints. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 343–358. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  14. Laviron, V., Logozzo, F.: SubPolyhedra: A (More) scalable approach to infer linear inequalities. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 229–244. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  15. Logozzo, F., Fähndrich, M.: On the relative completeness of bytecode analysis versus source code analysis. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 197–212. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Logozzo, F., Fähndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: ACM SAC 2008. ACM Press, New York (2008)

    Google Scholar 

  17. Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1991)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Francesco Logozzo

Authors
  1. Francesco Logozzo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. UC San Diego, USA

    Ranjit Jhala

  2. Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, 66506, Manhattan, KS, USA

    David Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Logozzo, F. (2011). Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation. In: Jhala, R., Schmidt, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2011. Lecture Notes in Computer Science, vol 6538. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18275-4_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-18275-4_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-18274-7

  • Online ISBN: 978-3-642-18275-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation