Skip to main content
Springer Nature Link
Log in

Java Automated Deductive Verification in Practice: Lessons from Industrial Proof-Based Projects

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice (ISoLA 2018)

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

Included in the following conference series:

Abstract

Formal methods in the form of automated proof-based deductive verification is increasingly used in industry to give confidence in the security and correctness of libraries and applications. This paper presents observations on current tools and processes based on recent experience with verification projects on industrial software: scalability, breadth, specification language expressibility and semantics, capabilities of underlying SMT tools, and integration into industrial build and continuous integration processes.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
CHF34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
CHF 24.95
Price includes VAT (Switzerland)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
CHF 47.00
Price excludes VAT (Switzerland)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
CHF 59.00
Price excludes VAT (Switzerland)
  • 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

Similar content being viewed by others

References

  1. Abrial, J.R., Hoare, A., Chapron, P.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  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. LNCS, vol. 10001. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-319-49812-6

    Book  Google Scholar 

  3. Barnes, J.: Spark: The Proven Approach to High Integrity Software. Altran Praxis, UK (2012). http://www.altran.co.uk

  4. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, England (2010)

    Google Scholar 

  5. Baudin, P.: ACSL: ANSI C Specification Language. http://frama-c.com/download/acsl_1.4.pdf

  6. Burdy, L., et al.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 80, pages 73–89. Elsevier, June 2003

    Google Scholar 

  7. Cok, D.R.: Observational purity by underspecification (and separation logic?). In Dagstuhl Conference, Typing, Analysis and Verification of Heap-Manipulating Programs (2009)

    Google Scholar 

  8. Cok, D.: Improved usability and performance of SMT solvers for debugging specifications. STTT 12, 467–481 (2010)

    Article  Google Scholar 

  9. Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_35

    Chapter  Google Scholar 

  10. Cok, D.R.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Workshop on Formal Integrated Development Environment (F-IDE 2014). EPTCS, vol. 149, pp. 79–92, Grenoble, France, 06 April 2014 (2014)

    Google Scholar 

  11. Cok, D.R.: Specification editing and discovery assistant for C/C++ software development. In: Nguyen, H., Steele, G. (eds.) SBIR Advanced Technologies in Aviation and Air Transportation System 2016 (2017)

    Google Scholar 

  12. Cok, D.R., Johnson, S.C.: SPEEDY: an eclipse-based ide for invariant inference. In: Electronic Proceedings in Theoretical Computer Science (EPTCS) (2014)

    Google Scholar 

  13. Cok, D.R., Kiniry, J.R.: ESC/Java2: uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_6

    Chapter  Google Scholar 

  14. Cok, D.R., Leavens, G.T.: Extensions of the theory of observational purity and a practical design for JML. In: Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008), pp. 43–50, November 2008. CS-TR-08-07 (2018)

    Google Scholar 

  15. Cok, D.R., Tasiran, S.: Practical Methods for Reasoning about Java 8’s Functional Programming Features. VSTTE 2018 (2018)

    Google Scholar 

  16. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  17. Garland, S.J., Guttag, J.V.: A guide to LP, the larch prover. Technical report 82, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, December 1991. Order from src-report@src.dec.com

    Google Scholar 

  18. Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. Technical report CS-TR-09-01, School of EECS, University of Central Florida, Orlando, March 2009

    Google Scholar 

  19. Jacobs, B., Kiniry, J., Warnier, M.: Java program verification challenges. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 202–219. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39656-7_8

    Chapter  Google Scholar 

  20. Kassios, I.T., Müller, P.: Modular specification and verification of delegation with SMT solvers. Technical report, ETH Zurich (2011)

    Google Scholar 

  21. Leavens, G.T., Leino, K.R.M., Müller, P.: Specification and verification challenges for sequential object-oriented programs. Form. Asp. Comput. 19(2), 159–189 (2007)

    Article  Google Scholar 

  22. Leavens, G.T., et al.: JML Reference Manual. Department of Computer Science, Iowa State University (2013). http://www.jmlspecs.org

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

  24. Meyer, B.: Object-Oriented Software Construction. Prentice Hall, New York (1988)

    Google Scholar 

  25. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Program. 62(3), 253–286 (2006)

    Article  MathSciNet  Google Scholar 

  26. Naumann, D.A.: Observational purity and encapsulation. Theor. Comput. Sci. 376(3), 205–224 (2007)

    Article  MathSciNet  Google Scholar 

  27. Parnas, D.L.: Tabular representation of relations. Technical report (1992)

    Google Scholar 

  28. Singleton, J.L., Leavens, G.T., Rajan, H., Cok, D.R.: Poster: an algorithm and tool to infer practical postconditions. In: 2018 IEEE/ACM 40th IEEE International Conference on Software Engineering Software Engineering (ICSE). IEEE (2018)

    Google Scholar 

  29. Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., London (1992)

    Google Scholar 

  30. https://frama-c.com

  31. Many papers regarding JML can be found on the JML. http://www.jmlspecs.org

  32. OpenJDK. http://www.openjdk.org

  33. http://www.openjml.org

  34. http://www.smtlib.org

  35. The Spec# web site gives code, documentation and papers. http://research.microsoft.com/SpecSharp/

  36. The work on C++ specification is part of the VESSEDIA project. The VESSEDIA project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No. 731453. https://vessedia.eu

Download references

Author information

Authors and Affiliations

  1. CEA, LIST, Software Safety and Security Laboratory, PC 174, 91191, Gif-sur-Yvette, France

    David R. Cok

Authors
  1. David R. Cok
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David R. Cok .

Editor information

Editors and Affiliations

  1. University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Cok, D.R. (2018). Java Automated Deductive Verification in Practice: Lessons from Industrial Proof-Based Projects. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science(), vol 11247. Springer, Cham. https://doi.org/10.1007/978-3-030-03427-6_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03427-6_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03426-9

  • Online ISBN: 978-3-030-03427-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation

  NODES
innovation 1
INTERN 6
Note 3
Project 6