# Changeset 514

Ignore:
Timestamp:
Feb 15, 2011, 10:58:58 AM (8 years ago)
Message:

more tidying

File:
1 edited

### Legend:

Unmodified
 r513 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. 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