Changeset 3637


Ignore:
Timestamp:
Mar 8, 2017, 12:25:31 PM (5 months ago)
Author:
mulligan
Message:

...

Location:
Papers/jar-cerco-2017
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.tex

    r3631 r3637  
    6868the Seventh Framework Programme for Research of the European Commission, under
    6969FET-Open grant number: 243881}}
    70 \subtitle{Certified resource analysis for a large fragment of C}
     70\subtitle{Source-level complexity analysis for a large fragment of C}
    7171\journalname{Journal of Automated Reasoning}
    7272\titlerunning{Certified Complexity}
  • Papers/jar-cerco-2017/introduction.tex

    r3636 r3637  
    5555Since modern compilers---as discussed previously---may compile each expression and statement occurrence in radically different ways, optimisations may change control flow, and the cost of an object code instruction may depend on the runtime state of hardware components like pipelines and caches, none of which are visible in the source code, it has not been clear how one could go about defining such a cost model.
    5656
    57 In this paper, we report on the scientific and technical contributions of the Certified Complexity (`CerCo') project, an EU-funded collaboration between the Universities of Bologna, Edinburgh, and Paris 7.
    58 
    59 We first present a uniform, precise cost model for a large fragment of the C programming language---\emph{CerCo C}, which is similar to early versions of \emph{CompCert C}.
     57In this paper, we report on the scientific and technical contributions of the Certified Complexity (`CerCo') project~\cite{cerco}, an EU FET-Open funded collaboration between the Universities of Bologna, Edinburgh, and Paris 7.
     58
     59We first present a uniform, precise cost model for a large fragment of the C programming language---\emph{CerCo C}, which is based on early versions of \emph{CompCert C}~\cite{compcert}.
    6060To define this cost model, we have developed a technical device, which we have dubbed \emph{the labelling approach}~\cite{labelling}, a technique to implement compilers that induce cost models on source programs by a very lightweight tracking of code changes through the compilation pipeline.
    6161
     
    136136decouple execution time from execution history by introducing randomisation.
    137137
    138 In CerCo~\cite{cerco} we do not address this problem, optimistically assuming
     138In CerCo we do not address this problem, optimistically assuming
    139139that improvements in low-level timing analysis or architecture will make
    140140verification feasible in the longer term.
Note: See TracChangeset for help on using the changeset viewer.