This paper describes a core component of Mobius' Trusted Code Base, the Mobius base logic. This program logic facilitates the transmission of certificates that are generated u...
This document contains the Isabelle/HOL sources underlying our paper A bytecode logic for JML and types [2], updated to Isabelle 2008. We present a program logic for a subset of s...