Certified Complexity

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.