Formalizing the Java Virtual Machine in Isabelle/HOL

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

Vorkommen: