Ian Stark

Certified Complexity

Roberto Amadio, Andrea Asperti, Nicolas Ayache, Brian Campbell, Dominic Mulligan, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark

In Science Beyond Fiction: Proceedings of the 2nd European Future Technologies Conference and Exhibition FET 11, Budapest, Hungary, 4–6 May 2011. Procedia Computer Science 7(2011):175–177.

Visit the publisher's page. Go to other papers, talks or my home page.

Find out more about Mobility and Security research at Edinburgh and the CerCo project in particular.


CerCo (‘Certified Complexity’) aims to develop tools for reasoning about intensional properties of programs written in high level languages. If successful, it will be possible to write correct hard real time programs and to formally prove, in a high level way, that programs meet all deadlines. Further, as many clock cycles as possible can be wrought from the processor by using a cost model that does not over-estimate.

Cost models for high level languages compiled to machine code are non-compositional. The cost model must be determined by the compilation process and must assign costs to instructions depending on context. Our approach — letting the compiler output the cost model — induces a precise cost model for the source program from the compilation process itself. Further, we must raise our level of trust in the (cost inducing) compiler. We plan to formally verify the compiler, proving it respects both intensional and extensional — w.r.t the cost model — properties of the source program.

  author =       {Roberto Amadio and Andrea Asperti and Nicolas Ayache and
                  Brian Campbell and Dominic Mulligan and Randy Pollack and
                  Yann R{\'e}gis-Gianas and Claudio Sacerdoti Coen and Ian
  title =        {Certified Complexity},
  journal =      {Procedia Computer Science},
  number =       {7},
  pages =        {175--177},
  year =         {2011},
  doi =          {10.1016/j.procs.2011.09.054},
  url =          {http://homepages.ed.ac.uk/stark/cerco.html},
  pdf =          {http://homepages.ed.ac.uk/stark/cerco.pdf},
  note =         {In \emph{Science Beyond Fiction: Proceedings of the 2nd
                  European Future Technologies Conference and Exhibition
                  FET~11, Budapest, Hungary, 4--6 May~2011}}

This research was supported by the European Commission through CerCo, project 243381 from the Future and Emerging Technologies (FET) initiative in the Information and Communication Technologies (ICT) component of the Seventh Research Framework Programme (FP7).

Page last modified: Monday 21 October 2013