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