BCV

• To: types@cis.upenn.edu
• Subject: BCV
• From: nipkow@informatik.tu-muenchen.de
• Date: Mon, 12 Jun 2000 13:52:45 +0000
• Sender: nipkow@informatik.tu-muenchen.de

The following new paper may be of interest to readers of this mailing list:

Verified Bytecode Verifiers
Tobias Nipkow

This paper presents another important step towards a complete formal
machine-checked design of the Java Virtual Machine. Using the theorem prover
Isabelle/HOL we have formalized and proved correct an executable bytecode
verifier in the style of Kildall's algorithm for a significant subset of the
JVM. First an abstract framework for proving correctness of data flow based
type inference algorithms for typed assembly languages is formalized. It is
shown that under certain conditions Kildall's algorithm yield a correct
bytecode verifier. Then the framework is instantiated with a model of the
JVM.

http://www.in.tum.de/~nipkow/pubs/bcv2.html

• Prev: Faculty post in foundations of computer science
• Next: CONCUR 2000: Call for Participation and Final Program
• Index(es):
  • Main
  • Thread