Changeset 514

Timestamp:

Feb 15, 2011, 10:58:58 AM (7 years ago)

Author:

mulligan

Message:

more tidying

File:

• Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) (2 diffs)

Deliverables/D4.1/ITP-Paper/itp-2011.tex

@@ -97 +97 @@
 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 +107 @@
 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 over-estimation 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 processor---using a cost model that does not over-estimate---as possible.
 
 Other applications of our approach are in the domain of compiler verification