Summer Studentships

LFCS offers Summer Studentships for undergraduates to do work related to current research. This is one project proposed for 2002; for more information see the list of proposed projects.

Mobile Resource Guarantees

Don Sannella, David Aspinall, Stephen Gilmore, Ian Stark

The Mobile Resource Guarantees project is building infrastructure for endowing mobile bytecode programs with certificates as to their resource consumption, taking the form of condensed formal proofs which can be checked by the recipient before running the program.

There are various opportunities for summer projects within this programme. Here are two possibilities:

• The proofs of resource consumption mentioned above will be built using proof rules in a logic for asserting resource-related properties of Java bytecode programs. The proof rules are designed to be sound with respect to a formal semantics of Java byte code. One way of establishing soundness is to encode the semantics in a theorem prover like Isabelle or PVS and show that the proof rules are theorems.

• Programs will be written in a high-level language and compiled to bytecode, with a proof generated at the same time via a type system for describing resource consumption of high-level code. The compiler being built by the project will be "transparent", meaning that it will be possible to calculate how a particular fragment of high-level code will translate into bytecode, and from that what its resulting resource usage will be. The compiler needs to be extended with optimisations, but the transparency constraint means that only optimisations whose effect can be determined statically will be of interest.

If you are interested, please contact Don Sannella and look at the MRG project web site.