Skip to main content
SpringerLink
Log in

A Certified Implementation on Top of the Java Virtual Machine

  • Conference paper
Formal Methods for Industrial Critical Systems (FMICS 2009)

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

Abstract

Safe is a first-order functional language with unusual memory management features: memory can be both explicitly and implicitly deallocated at some specific points in the program text, and there is no need for a runtime garbage collector. The final code is bytecode of the Java Virtual Machine (JVM), so the language is useful for programming small devices based on this machine.

As an intermediate stage in the compiler’s back-end, we have defined the Safe Virtual Machine (SVM), and have implemented this machine on top of the Java Virtual Machine (JVM). The paper presents the certified implementation of the SVM on top of the JVM. We have used the proof assistant Isabelle/HOL for this purpose.

Partially supported by the Spanish and Madrid Region Government grants S-0505/TIC/0407 (PROMESAS), and TIN2008-06622-C03-01/TIN (STAMP).

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. Berghofer, S., Strecker, M.: Extracting a formally verified, fully executable compiler from a proof assistant. In: Proc. Compiler Optimization Meets Compiler Verification, COCV 2003. ENTCS, pp. 33–50 (2003)

    Google Scholar 

  2. Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. EATCS. Springer, Heidelberg (2004)

    Google Scholar 

  3. Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 460–475. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Software Engineering Notes 28(6), 2 (2003)

    Article  Google Scholar 

  5. de Dios, J., Peña, R.: Formal Certification of a Resource-Aware Language Implementation. In: Berghofer, S., et al. (eds.) TPHOL 2009. LNCS, vol. 5674, pp. 196–212. Springer, Heidelberg (2009)

    Google Scholar 

  6. Klein, G.: Verified Java Bytecode Verification, PhD thesis, Institut für Informatik, Technische Universität München (2003)

    Google Scholar 

  7. Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science 298, 583–626 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  8. Klein, G., Nipkow, T.: A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler. ACM Transactions on Programming Languages and Systems 28(4), 619–695 (2006)

    Article  Google Scholar 

  9. Klein, G., Nipkow, T., Schirmer, N., Strecker, M., Wildmoser, M.: Project VerifiCard (2001–2003), http://isabelle.in.tum.de/VerifiCard/

  10. Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Principles of Programming Languages, POPL 2006, pp. 42–54. ACM Press, New York (2006)

    Google Scholar 

  11. Leroy, X.: A formally verified compiler back-end, 79 pages (July 2008) (submitted)

    Google Scholar 

  12. Li, G., Owens, S., Slind, K.: Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 205–219. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. Lindholm, T., Yellin, F.: The Java Virtual Machine Sepecification, 2nd edn. The Java Series. Addison-Wesley, Reading (1999)

    Google Scholar 

  14. Montenegro, M., Peña, R., Segura, C.: A Simple Region Inference Algorithm for a First-Order Functional Language. In: Trends in Functional Programming, TFP 2008, Nijmegen (The Netherlands), May 2008, pp. 194–208 (2008)

    Google Scholar 

  15. Montenegro, M., Peña, R., Segura, C.: A Type System for Safe Memory Management and its Proof of Correctness. In: ACM Principles and Practice of Declarative Programming, PPDP 2008, Valencia, Spain, July 2008, pp. 152–162 (2008)

    Google Scholar 

  16. Montenegro, M., Peña, R., Segura, C.: An Inference Algorithm for Guaranteeing Safe Destruction. In: Selected papers of Logic-Based Program Sinthesis and Transformation, LOPSTR 2008. LNCS, vol. 5438, pp. 135–151. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. Necula, G.C.: Proof-Carrying Code. In: ACM SIGPLAN-SIGACT Principles of Programming Languages, POPL 1997, pp. 106–119. ACM Press, New York (1997)

    Chapter  Google Scholar 

  18. Necula, G.C.: Translation validation for an optimizing compiler. SIGPLAN Notices 35(5), 83–94 (2000)

    Article  Google Scholar 

  19. Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  20. Peña, R., Segura, C., Montenegro, M.: A Sharing Analysis for SAFE. In: Selected Papers of the 7th Symp. on Trends in Functional Programming, TFP 2006, pp. 109–128. Intellect, Bristol (2007)

    Google Scholar 

  21. Pnueli, A., Siegel, M., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  22. Pusch, C.: Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 89–103. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  23. Strecker, M.: Formal Verification of a Java Compiler in Isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 63–77. Springer, Heidelberg (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid,  

    Javier de Dios & Ricardo Peña

Authors
  1. Javier de Dios
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ricardo Peña
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DSIC/ELP, Universidad Politécnica de Valencia, Camino de Vera s/n, 46022, Valencia, Spain

    María Alpuente  & Christophe Joubert  & 

  2. Microsoft Research, Roger Needham Building, J J Thomson Avenue, CB3 0FB, Cambridge, UK

    Byron Cook

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Dios, J., Peña, R. (2009). A Certified Implementation on Top of the Java Virtual Machine. In: Alpuente, M., Cook, B., Joubert, C. (eds) Formal Methods for Industrial Critical Systems. FMICS 2009. Lecture Notes in Computer Science, vol 5825. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04570-7_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04570-7_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04569-1

  • Online ISBN: 978-3-642-04570-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation