Skip to main content
SpringerLink
Log in

Translating Scala Programs to Isabelle/HOL

System Description

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2016)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9706))

Included in the following conference series:

Abstract

We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs) stemming from the input program. Isabelle, on the other hand, is an interactive theorem prover used to verify mathematical specifications using its own input language Isabelle/Isar. Users specify (inductive) definitions and write proofs about them manually, albeit with the help of semi-automated tactics. The integration of these two systems allows us to exploit Isabelle’s rich standard library and give greater confidence guarantees in the correctness of analysed programs.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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

Notes

  1. 1.

    Because our implementation uses Isabelle in interactive instead of in batch mode, we cannot produce pre-computed heap images to be loaded for later runs.

  2. 2.

    The full example is available at https://git.io/vznVH.

  3. 3.

    In fact, while attempting to implement array support we discovered that Leon’s purely functional view of immutably used arrays does not respect Scala’s reference equality implementation of arrays, leading to a decision to disallow array equality in Leon’s Pure Scala.

  4. 4.

    https://github.com/epfl-lara/leon.

References

  1. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  2. Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Scala Workshop (2013)

    Google Scholar 

  3. Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93–110. Springer, Heidelberg (2014)

    Google Scholar 

  4. Breitner, J., Huffman, B., Mitchell, N., Sternagel, C.: Certified HLints with Isabelle/HOLCF-Prelude, Haskell and Rewriting Techniques (HART), June 2013

    Google Scholar 

  5. Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technische Universität München (2009)

    Google Scholar 

  6. Haftmann, F.: From higher-order logic to Haskell: there and back again. In: Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 155–158. ACM (2010)

    Google Scholar 

  7. Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Haller, P., Prokopec, A., Miller, H., Klang, V., Kuhn, R., Jovanovic, V.: Futures and promises (2012). http://docs.scala-lang.org/overviews/core/futures.html

  9. Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reason. 44(4), 303–336 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  10. Kuncak, V.: Developing verified software using Leon. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 12–15. Springer, Heidelberg (2015)

    Google Scholar 

  11. Kunčar, O.: Correctness of Isabelle’s cyclicity checker: implementability of overloading in proof assistants. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, pp. 85–94. ACM, New York (2015)

    Google Scholar 

  12. Mehnert, H.: Kopitiam: modular incremental interactive full functional static verification of java code. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 518–524. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  14. Nipkow, T., Klein, G.: Concrete Semantics. Springer, New York (2014)

    Book  MATH  Google Scholar 

  15. Odersky, M., Spoon, L., Venners, B.: Programming in Scala, 2nd edn. Artima Inc, Walnut Creek (2010)

    Google Scholar 

  16. Terdoslavich, W.: IBM bets on apache spark as ’the future of enterprise data’. http://www.informationweek.com/big-data/ibm-bets-on-apache-spark-as-the-future-of-enterprise-data/d/d-id/1320855

  17. Voirol, N., Kneuss, E., Kuncak, V.: Counter-example complete verification for higher-order functions. In: Scala Symposium (2015)

    Google Scholar 

  18. Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 244–259. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Wenzel, M.: Isabelle/jEdit – a prover IDE within the PIDE framework. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 468–471. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  20. Wenzel, M.: The Isabelle/Isar Reference Manual (2013)

    Google Scholar 

  21. Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515–530. Springer, Heidelberg (2014)

    Google Scholar 

Download references

Acknowledgements

We would like to thank the people who helped “making the code work”: Ravi Kandhadai, Etienne Kneuss, Manos Koukoutos, Mikäel Mayer, Nicolas Voirol, Makarius Wenzel. Cornelius Diekmann, Manuel Eberl, and Tobias Nipkow suggested many textual improvements to this paper.

Author information

Authors and Affiliations

  1. Technische Universität München, München, Germany

    Lars Hupel

  2. École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland

    Viktor Kuncak

Authors
  1. Lars Hupel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Viktor Kuncak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lars Hupel .

Editor information

Editors and Affiliations

  1. Aix-Marseille University, Marseille, France

    Nicola Olivetti

  2. SRI International, Menlo Park, California, USA

    Ashish Tiwari

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Hupel, L., Kuncak, V. (2016). Translating Scala Programs to Isabelle/HOL. In: Olivetti, N., Tiwari, A. (eds) Automated Reasoning. IJCAR 2016. Lecture Notes in Computer Science(), vol 9706. Springer, Cham. https://doi.org/10.1007/978-3-319-40229-1_38

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40229-1_38

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40228-4

  • Online ISBN: 978-3-319-40229-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation