Benutzer: Gast  Login
Titel:

Formalizing the Java Virtual Machine in Isabelle/HOL

Dokumenttyp:
Technical Report
Autor(en):
Cornelia Pusch
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