This directory contains documents for the presentation of the project
in the dissemination workshops and in the final review.

Each module is supposed to last between 15' and 30', so it should be
supported by a set of 15-30 slides and possibly by a short demo.

Not all modules need to be presented each time.

Module:
Overview
Abstract (*To come (Bologna?)*)

Module:
The labelling approach to certified cost annotations.
Abstract 
We present a so-called labelling method to enrich a compiler in order
to turn it into a ``cost annotating compiler'', that is, a compiler
which can ``lift'' pieces of information on the execution cost of the
object code as cost annotations on the source code. These cost
annotations characterize the execution costs of code fragments of
constant complexity.  First, we provide a proof methodology that
extends standard simulation proofs of compiler correctness to ensure
that the cost annotations on the source code are sound and precise
with respect to an execution cost model of the object code.  Second,
we demonstrate that our label-based instrumentation is scalable
because it consists in a modular extension of the compilation
chain. To that end, we report our successful experience in
implementing and testing the labelling approach on top of a prototype
compiler written in OCAML for (a large fragment of) the C language.

Module: 
Reasoning on cost annotations of C programms.
Abstract 
We provide evidence for the usability of the generated cost
annotations as a mean to reason on the concrete complexity of programs
written in C. For this purpose, we present a Frama-C plugin that uses
our cost annotating compiler to automatically infer trustworthy logic
assertions about the concrete worst case execution cost of programs
written in a fragment of the C language. These logic assertions are
synthetic in the sense that they characterize the cost of executing
the entire program, not only constant-time fragments. (These bounds
may depend on the size of the input data.) We report our
experimentations on some C programs, including programs generated by a
compiler for the synchronous programming language Lustre used in
critical embedded software.


Module:
Targeting more advanced optimisations: indexed labelling.
Abstract
We present an extension to the labelling approach. The original approach looses
preciseness when differences arise as to the cost of the same portion of code,
whether due to code transformation such as loop optimisations or advanced
architecture features (e.g. cache). We propose to address this weakness by
formally indexing cost labels with the iterations of the containing loops they
occur in. These indexes can be transformed during the compilation, and when
lifted back to source code they produce dependent costs.
The proposed changes have been implemented in CerCo's untrusted prototype
compiler.

Module:
Certifying and reasoning on cost annotations of functional programs.
Abstract 
We design a labelling method to insert cost annotations in a
higher-order functional program, to certify their correctness with
respect to a standard, typable compilation chain to assembly code
including safe memory management, and to reason about them in a
higher-order Hoare logic.
Slides: funcca-slide.pdf

Module:
Compiler certification in Matita (tentative title, add more modules if needed...)
Abstract (*To come (Edinburgh/Bologna?)*)