Skip to main content
SpringerLink
Log in
Book cover

Formal Methods Teaching Workshop

FMTea 2019: Formal Methods Teaching pp 37–51Cite as

Using Krakatoa for Teaching Formal Verification of Java Programs

  • Conference paper
  • First Online:

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

Abstract

In this work, we present a study of different support tools to teach formal verification of Java programs and show our experience with Krakatoa, an automatic theorem prover based on Hoare logic which allows students to interactively visualize the different steps required to prove the correctness of a program, to think about the used reasoning and to understand the importance of verification of algorithms to improve the reliability of our programs.

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

Learn about institutional subscriptions

Notes

  1. 1.

    http://www.cse.chalmers.se/edu/year/2018/course/TDA294_Formal_Methods_for_Software_Development/.

  2. 2.

    https://formal.iti.kit.edu/teaching/FormSys2SoSe2017/.

  3. 3.

    Alt-Ergo http://alt-ergo.lri.fr/.

  4. 4.

    CVC3 http://www.cs.nyu.edu/acsys/cvc3/.

References

  1. Common Criteria for Information Technology Security Evaluation. Technical report (2012)

    Google Scholar 

  2. Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. Lecture Notes in Computer Science, vol. 10001. Springer, Berlin (2016). https://doi.org/10.1007/978-3-319-49812-6

    Book  Google Scholar 

  3. Barthe, G., et al.: 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). https://doi.org/10.1007/978-3-540-74792-5_7

    Chapter  Google Scholar 

  4. Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: Using first-order theorem provers in the Jahob data structure verification system. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 74–88. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69738-1_5

    Chapter  MATH  Google Scholar 

  5. Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Proceedings of the Third International Conference on NASA Formal Methods, pp. 472–479. NFM 2011 (2011)

    Google Scholar 

  6. Coq development team: The Coq Proof Assistant, version 8.9.1. Technical report (2019). https://coq.inria.fr/

  7. Feinerer, I., Salzer, G.: Automated tools for teaching formal software verification. In: Proceedings of the 2006 Conference on Teaching Formal Methods: Practice and Experience, p. 4 (2006)

    Google Scholar 

  8. Filliâtre, J.C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Proceedings of the 19th International Conference on Computer Aided Verification, pp. 173–177. CAV 2007 (2007)

    Google Scholar 

  9. 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). https://doi.org/10.1007/978-3-642-37036-6_8

    Chapter  Google Scholar 

  10. Gary T., Leavens, A.L.B., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. Technical report (2000), iowa State University

    Google Scholar 

  11. Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transf, 2(4), 366–381 (2000)

    Article  Google Scholar 

  12. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969)

    Article  Google Scholar 

  13. Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207–220. ACM (2009)

    Google Scholar 

  14. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20

    Chapter  MATH  Google Scholar 

  15. Poll, E.: Teaching program specification and verification using JML and ESC/Java2. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 92–104. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_7

    Chapter  Google Scholar 

  16. Romero, A.: El uso de los demostradores automáticos de teoremas para la enseñanza de la programación. In: Proceedings of Jornadas de Enseñanza Universitaria de la Informática (JENUI 2013) (2013)

    Google Scholar 

  17. Sznuk, T., Schubert, A.: Tool support for teaching Hoare logic. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 332–346. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10431-7_27

    Chapter  Google Scholar 

  18. T. Nipkow, M. Wenzel, L.C.P.: Isabelle 2019 (2019). https://isabelle.in.tum.de/

Download references

Acknowledgments

Partially supported by the Spanish Ministry of Science, Innovation and Universities, project MTM2017-88804-P.

Author information

Authors and Affiliations

  1. University of La Rioja, Logroño, Spain

    Jose Divasón & Ana Romero

Authors
  1. Jose Divasón
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ana Romero
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ana Romero .

Editor information

Editors and Affiliations

  1. University of Surrey, Guildford, UK

    Brijesh Dongol

  2. Åbo Akademi University, Turku, Finland

    Luigia Petre

  3. The University of Queensland, Brisbane, QLD, Australia

    Graeme Smith

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Divasón, J., Romero, A. (2019). Using Krakatoa for Teaching Formal Verification of Java Programs. In: Dongol, B., Petre, L., Smith, G. (eds) Formal Methods Teaching. FMTea 2019. Lecture Notes in Computer Science(), vol 11758. Springer, Cham. https://doi.org/10.1007/978-3-030-32441-4_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32441-4_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32440-7

  • Online ISBN: 978-3-030-32441-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation