Version 1 (modified by sacerdot, 7 years ago) (diff)


List of milestones and planning of reviews

We have one milestone every 12 months. After the first year we plan to have a functional prototype of a cost annotating compiler, written in OCaml. At the end of the second year, a mature version of the compiler will have been encoded in CIC together with an executable specification (interpreter) of the source, intermediate and target language. At the end of the project we will deliver a completely certified version of the cost annotating compiler, together with a proof of concept implementation of a system that exploits the cost annotations to verify the actual complexity of compiled programs.

See Workplan Table WT4: List of milestones and Workplan Table WT5: Tentative schedule of Project Reviews.