Chapter 14 Project Evaluation Paper : Mobile Resource Guarantees

The Mobile Resource Guarantees (MRG) project has developed a proof-carrying-code infrastructure for certifying resou rce bounds of mobile code. Key components of this infrastructure are a certifying comp iler for a high-level language, a hierarchy of program logics, tailored for reaso ning about resource consumption, and an embedding of the logics into a theorem pr over. In this paper, we give an overview of the project’s results, discuss the les son learnt from it and introduce follow-up work in new projects that will build on t hese results.