User: Guest  Login
Title:

Formalizing the Java Virtual Machine in Isabelle/HOL

Document type:
Technical Report
Author(s):
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.
Keywords:
Java; JVM; Isabelle; Formal Verification
Year:
1998
Year / month:
1998-06-01 00:00:00
Pages:
43
 BibTeX