Logics for Certifying Resource Bounds

Photograph of David Aspinall

David Aspinall

(Edinburgh)

The Mobile Resource Guarantees (MRG) project is developing Proof-Carrying Code technology to endow mobile code with certificates of bounded resource consumption. These certificates are generated by a compiler which, in addition to translating high-level programs into byte code, derives formal proofs based on programmer annotations and program analysis.

As the basis for reasoning and certificate generation, we employ a program logic for a subset of the JVM, implemented in Isabelle/HOL. This logic has good properties, including mechanized formal proofs of soundness and (relative) completeness. However, it proved to be rather low level for direct automatic use. To address this we have defined a derived assertion format which relates directly to the compile time analysis, which has simple side conditions that make automatic verification feasible.

In this talk I will present the program logic of MRG and also explain the derived assertions. The presentation follows on from a Swansea Colloquium in November 2003 given by Don Sannella, but a perfectly accurate memory of that talk will not be assumed.
Thursday 11th November 2004, 14:00
Robert Recorde Room
Department of Computer Science