Skip to main content
SpringerLink
Log in

Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code

  • Conference paper
Book cover NASA Formal Methods (NFM 2011)

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

Included in the following conference series:

Abstract

We are developing Kopitiam, a tool to interactively prove full functional correctness of Java programs using separation logic by interacting with the interactive theorem prover Coq. Kopitiam is an Eclipse plugin, enabling seamless integration into the workflow of a developer. Kopitiam enables a user to develop proofs side-by-side with Java programs in Eclipse.

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. Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling 4 (2005)

    Google Scholar 

  2. Appel, A.W.: Tactics for separation logic. INRIA Rocquencourt and Princeton University, Early Draft (2006)

    Google Scholar 

  3. Barthe, G., Crégut, P., Grégoire, B., Jensen, T., Pichardie, D.: The MOBIUS proof carrying code infrastructure. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.P. (eds.) Formal Methods for Components and Objects. Springer, Heidelberg (2008)

    Google Scholar 

  4. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. In: Coq’Art: the Calculus of Inductive Constructions. Springer, Heidelberg (2004)

    Google Scholar 

  5. Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer 7 (June 2005), also published by Springer http://dx.doi.org/10.1007/s10009-004-0167-4

  6. Charles, J., Kiniry, J.R.: A lightweight theorem prover interface for Eclipse. UITP at TPHOL 2008 (2008)

    Google Scholar 

  7. Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: ACM Proc. of ICFP 2009 (August 2009)

    Google Scholar 

  8. Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: ACM Proc. of OOPSLA 2008 (October 2008)

    Google Scholar 

  9. Driscoll, J., Sarnak, N., Sleator, D., Tarjan, R.: Making data structures persistent. In: ACM Proc. of STOC 1986 (November 1986)

    Google Scholar 

  10. Fähndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: ACM Proc. of SAC 2010 (March 2010)

    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. Jensen, J.B., Birkedal, L., Sestoft, P.: Modular verification of linked lists with views via separation logic. In: Proc. of FTfJP 2010 (May 2010)

    Google Scholar 

  13. Kokholm, N., Sestoft, P.: The C5 generic collection library for C# and CLI. Tech. Rep. ITU-TR-2006-76, IT University of Copenhagen (2006)

    Google Scholar 

  14. Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Proc. of LPAR-16 (March 2010)

    Google Scholar 

  15. Meyer, B.: Design by contract. In: Advances in Object-Oriented Software Engineering (1991)

    Google Scholar 

  16. Odersky, M., et al.: An overview of the Scala programming language. Tech. Rep. IC/2004/64, EPFL Lausanne, Switzerland (2004)

    Google Scholar 

  17. Parkinson, M.J., Bierman, G.: Separation logic, abstraction and inheritance. In: ACM Proc. of POPL 2008 (January 2008)

    Google Scholar 

  18. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: IEEE Proc. of 17th Symp. on Logic in CS (November 2002)

    Google Scholar 

  19. Vallée-Rai, R., Hendren, L.J.: Jimple: Simplifying Java bytecode for analyses and transformations. Tech. Rep. 4, McGill University (1998)

    Google Scholar 

  20. Weide, B., Sitaraman, M., Harton, H., Adcock, B., Bucci, P., Bronish, D., Heym, W., Kirschenbaum, J., Frazier, D.: Incremental benchmarks for software verification tools and techniques. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 84–98. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IT University of Copenhagen, 2300, København S, Denmark

    Hannes Mehnert

Authors
  1. Hannes Mehnert
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA Jet Propulsion Laboratory, 4800 Oak Grove Drive, M/S 301-285, 91109, Pasadena, CA, USA

    Mihaela Bobaru , Klaus Havelund , Gerard J. Holzmann  & Rajeev Joshi , ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mehnert, H. (2011). Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-20398-5_42

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-20397-8

  • Online ISBN: 978-3-642-20398-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation