Mobile Resource Guarantees

Donald Sannella; Martin Hofmann; David Aspinall; Stephen Gilmore; Ian Stark; Lennart Beringer; Hans-Wolfgang Loidl; Kenneth MacKenzie; Alberto Momigliano; Olha Shkaravska

Mobile Resource Guarantees

Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, Olha Shkaravska

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Trends in Functional Programming
Publisher	Intellect
Pages	211-226
Number of pages	16
Volume	6
Publication status	Published - 2007

Access to Document

Sannella Hofmann ET AL 2007 Project Evaluation Paper Mobile Resource GuaranteesAccepted author manuscript, 121 KB

Cite this

@inproceedings{617dba34e77b4f4dae2a02c5080a653a,

title = "Mobile Resource Guarantees",

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.",

author = "Donald Sannella and Martin Hofmann and David Aspinall and Stephen Gilmore and Ian Stark and Lennart Beringer and Hans-Wolfgang Loidl and Kenneth MacKenzie and Alberto Momigliano and Olha Shkaravska",

year = "2007",

language = "English",

volume = "6",

pages = "211--226",

booktitle = "Trends in Functional Programming",

publisher = "Intellect",

}

TY - GEN

T1 - Mobile Resource Guarantees

AU - Sannella, Donald

AU - Hofmann, Martin

AU - Aspinall, David

AU - Gilmore, Stephen

AU - Stark, Ian

AU - Beringer, Lennart

AU - Loidl, Hans-Wolfgang

AU - MacKenzie, Kenneth

AU - Momigliano, Alberto

AU - Shkaravska, Olha

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

M3 - Conference contribution

VL - 6

SP - 211

EP - 226

BT - Trends in Functional Programming

PB - Intellect

ER -

Mobile Resource Guarantees

Abstract

Access to Document

Fingerprint

Cite this