Links und Funktionen

You are here: Home / Publikationen / A Bytecode Logic for JML and Types


Lennart Beringer and Martin Hofmann (2006)

A Bytecode Logic for JML and Types

In: Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings, ed. by Naoki Kobayashi, vol. 4279, pp. 389-405, Springer. Lecture Notes in Computer Science (ISBN: 3-540-48937-1).

We present a program logic for virtual machine code that may serve as a suitable target for different proof-transforming compilers. Compilation from JML-specified source code is supported$~$ by the inclusion of annotations whose interpretation extends to non-terminating computations. Compilation from functional languages, and the communication of results from intermediate$~$ level program analysis phases are facilitated by a new judgement format that admits the compositionality of type systems to be reflected in derivations. This makes the logic well suited to$~$ serve as a language in which proofs of a PCC architecture are expressed. We substantiate this claim by presenting the compositional encoding of a type system for bounded heap$~$ consumption. Both the soundness proof of the logic and the derivation of the type system have been formally verified by an implementation in Isabelle/HOL.

Document Actions