1. Chapter 14: Project Evaluation Paper: Mobile Resource Guarantees.
- Author
-
Sannella, Donald, Hofmann, Martin, Aspinall, David, Gilmore, Stephen, Stark, Ian, Beringer, Lennart, Loidl, Hans-Wolfgang, MacKenzie, Kenneth, Momigliano, Alberto, and Shkaravska, Olha
- Subjects
INFORMATION superhighway ,CIPHERS ,COMPILERS (Computer programs) ,COMPUTER logic ,PROGRAMMING languages - Abstract
The Mobile Resource Guarantees (MRG) project has developed a proof-carrying-code infrastructure for certifying resource bounds of mobile code. Key components of this infrastructure are a certifying compiler for a high-level language, a hierarchy of program logics, tailored for reasoning about resource consumption, and an embedding of the logics into a theorem prover. In this paper, we give an overview of the project's results, discuss the lessons learnt from it and introduce follow-up work in new projects that will build on these results. [ABSTRACT FROM AUTHOR]
- Published
- 2007