Changeset 3450 for Papers

Ignore:
Timestamp:
Feb 20, 2014, 11:26:04 AM (6 years ago)
Message:

small rewordings of the abstract, working on rest of paper

File:
1 edited

Legend:

Unmodified
 r3444 % in the dependent labelling section. \begin{abstract} This paper provides an overview of the FET-Open Project CerCo (Certified Complexity'). The project's main achievement is We provide an overview of the FET-Open Project CerCo (Certified Complexity'). Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level, with little or no loss of accuracy and with a small trusted code base. The main software component developed is a certified compiler producing cost annotations. The compiler translates source code to object code and produces an instrumented copy of the source code. This instrumentation exposes at the source level---and tracks precisely---the actual (non-asymptotic) properties of programs (time, space) at the source level, with little or no loss of accuracy, and with a small trusted code base. We developed a certified compiler that translates C source code to object code, producing a copy of the source code instrumented with cost annotations as an additional side-effect. These instrumentations expose at the source level---and track precisely---the actual (non-asymptotic) computational cost of the input program. Untrusted invariant generators and trusted theorem provers can then be used to compute and certify the parametric execution time of the may then be used to compute and certify the parametric execution time of the code. \end{abstract}