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

small rewordings of the abstract, working on rest of paper

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3444 r3450  
    9494% in the dependent labelling section.
    9595\begin{abstract}
    96 This paper provides an overview of the FET-Open Project CerCo
    97 (`Certified Complexity'). The project's main achievement is
     96We provide an overview of the FET-Open Project CerCo
     97(`Certified Complexity'). Our main achievement is
    9898the development of a technique for analysing non-functional
    99 properties of programs (time, space) at the source level, with little or no loss of accuracy
    100 and with a small trusted code base. The main software component
    101 developed is a certified compiler producing cost annotations. The compiler
    102 translates source code to object code and produces an instrumented copy of the
    103 source code. This instrumentation exposes at
    104 the source level---and tracks precisely---the actual (non-asymptotic)
     99properties of programs (time, space) at the source level, with little or no loss of accuracy,
     100and 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
     101the source level---and track precisely---the actual (non-asymptotic)
    105102computational cost of the input program. Untrusted invariant generators and trusted theorem provers
    106 can then be used to compute and certify the parametric execution time of the
     103may then be used to compute and certify the parametric execution time of the
    107104code.
    108105\end{abstract}
Note: See TracChangeset for help on using the changeset viewer.