Related national and international research activities
During the development of the project we shall devote a particular attention to the evolution of related research efforts.
A closely related one is INRIA's http://pauillac.inria.fr/�xleroy/compcert/CompCert, the certified compiler written in Coq by X. Leroy and his team. As for CerCo, the source language of CompCert is a large subset of C. The target language of CompCert is PowerPC assembly and several intermediate data structures and phases of the back-end are tightly bound to this choice. For instance, instruction selection is performed in the first phase of the back-end and pseudo-registers are partitioned into floating point and standard registers to match the actual machine registers in later phases. In CompCert we plan to address simpler microprocessors of the type frequently used for embedded systems. Moreover, the additional constraints imposed by the preservation of complexity could also prevent sharing of data structures and intermediate languages among the two projects. Nevertheless, the work done in Compcert will be a major source of inspiration.
Another INRIA's project we plan to collaborate with is http://www.inria.fr/recherche/equipes/proval.fr.htmlProval, in charge of the development the Why-Caduceus deductive platform, in view of the possible use of this tool for the proof-of-concept prototype of WPround(4+1:0). In particular, Caduceus and Why allow to generate proof obligation for C programs annotated with preconditions, postconditions and loop invariants. The obligations can be feed to several automated or interactive theorem provers to be solved. As a proof of concept for the exploitation of CerCo, we plan in WPround(4+1:0)to use these or similar systems to generate proof obligations for complexity invariants derived from the cost annotations produced by the CerCo compiler. We will also explore in Task Tround(4.2+1:1)the possibility of helping the user in proving these obligations by increasing automation.
Our project is also related to the CMU/Penn http://www.cis.upenn.edu/�plclub/ms/index.htmlManifest Security Initiative. Its research objectives are
to develop the theoretical foundations for manifestly secure software and to demonstrate its feasibility in practice. As a matter of fact, a possible application of CerCo is to proof carrying code techniques, allowing to specify the computational cost of untrusted and potentially malicious extensions, along with a proof of their complexity.
The http://alliance.seas.upenn.edu/�plclub/cgi-bin/poplmark/index.php?title=The_POPLmark_ChallengePoplmark Challenge, proposed by the University of Pennsylvania, is a set of benchmarks designed to evaluate mechanized theorem proving tools in the setting of the metatheory of programming languages. The benchmarks are drawn from the metatheory of a simple dialect of the lambda calculus, hence are focused on small scale formalization of programming languages. Even though our effort aims at a much larger scale certification, we expect that the experience gathered in the Poplmark Challenge might turn useful, particularly in the issues of name binding and complex induction principles.
INRIA-Microsoft's Mathematical Components project aims to demonstrate that formalized mathematical theories can, like modern software, be built out of components. Their effort is not only toward the formalization of finite group theory up to the odd order theorem, an ambitious challenge and a good test case, but also in the development of modular tools to make it possible to formalize such huge proofs. To pursue this last objective they started from http://www.msr-inria.inria.fr/Projects/math-componentsSSReflect, a proof shell extending the Coq system developed by Gonthier to carry out the formalization of the Four Colour Theorem. SSReflect comes with a modular library of theorems conceived to reason about structures equipped with a decidable equality and a highly flexible set of commands specifically designed to carry out huge proofs in that domain. While structures with a decidable equality appear in a quite small part of mainstream mathematics, they are ubiquitous in the field of programming, and consequently in the implementation of a compiler. For that reason the technology developed by the Mathematical Components team seems an interesting device we may adopt, possibly tailoring it to our needs collaborating with them.
Our project is complementary to the http://www-fp.cs.st-andrews.ac.uk/embounded/pubs/hume/embounded-tfp05.pdfEmbound Project of the sixth Programme Framework. While the main focus of Embound was on static analysis techniques for Worst Case Analysis of real time systems, our project is aimed at building a verified infrastructure allowing to translate a high level analysis of the source program into a faithful counterpart on its executable. Moreover, while Embound started from a functional based, domain specific language as Hume, ending into a virtual abstract machine (HAM), we start from C and end up to the hardware. The methodology is also different: Embound was based on resource bound computational techniques that in recent years have clearly proved their limitations: we impose no restriction on the kind of techniques used to prove the complexity bounds, focusing our attention on the translation of computational costs from the source to the target, and proving its correctness.