Index: /Deliverables/D4.1/ITPPaper/itp2011.tex
===================================================================
 /Deliverables/D4.1/ITPPaper/itp2011.tex (revision 513)
+++ /Deliverables/D4.1/ITPPaper/itp2011.tex (revision 514)
@@ 97,5 +97,4 @@
To what extent can you trust your compiler in preserving those properties?
\end{itemize*}

These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification}.
So far, the field has been focused on the first and last questions only.
@@ 108,14 +107,13 @@
Therefore both the cost model and intensional specifications are affected by the compilation process.
In the EU Project CerCo (Certified Complexity) we will approach the problem
by developing a compiler that induces the cost model on the source code by
assigning to each block of high level instructions the cost associated to the
obtained object code. The cost model will thus be inherently non compositional,
but it can be extremely \emph{precise}, capturing the realistic cost. In
particular, we already have a prototype where no approximation of the cost
is provided at all. The natural applications of our approach are then in the
domain of hard real time programs, where the user can certify the meeting of
all dealines while fully exploiting the computational time, that would be
wasted in case of overestimation of the costs.
+In the current EU Project CerCo (`Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows.
+We are currently developing a compiler that induces a cost model on the high level source code.
+Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled object code.
+The cost model is therefore inherently non compositional.
+However, the model has the potential to be extremely \emph{precise}, capturing a program's \emph{realistic} cost, by taking into account, not ignoring, the compilation process.
+A prototype compiler, where no approximation of the cost is provided, has been developed.
+
+We believe that our approach is especially applicable to certifying real time programs.
+Here, a user can certify that all `deadlines' are met whilst wringing as many clock cycles from the processorusing a cost model that does not overestimateas possible.
Other applications of our approach are in the domain of compiler verification