Login
- Dokumenttyp:
- Technical Report
- Autor(en):
- Cornelia Pusch
- Titel:
- Formalizing the Java Virtual Machine in Isabelle/HOL
- Abstract:
- We present a formalization of the central parts of the Java Virtual Machine (JVM) with the theorem prover Isabelle/HOL. We formalize the class file format and give an operational semantics for a nontrivial subset of JVM instructions, covering the central parts of object oriented programming.
- Stichworte:
- Java; JVM; Isabelle; Formal Verification
- Jahr:
- 1998
- Jahr / Monat:
- 1998-06-01 00:00:00
- Seiten/Umfang:
- 43
BibTeX