Changeset 3637 for Papers/jar-cerco-2017

Timestamp:

Mar 8, 2017, 12:25:31 PM (3 years ago)

Author:

mulligan

Message:

...

Location:

Papers/jar-cerco-2017

Files:

• cerco.tex (modified) (1 diff)
• introduction.tex (modified) (2 diffs)

Papers/jar-cerco-2017/cerco.tex

@@ -68 +68 @@
 the Seventh Framework Programme for Research of the European Commission, under 
 FET-Open grant number: 243881}}
-\subtitle{Certified resource analysis for a large fragment of C}
+\subtitle{Source-level complexity analysis for a large fragment of C}
 \journalname{Journal of Automated Reasoning}
 \titlerunning{Certified Complexity}

Papers/jar-cerco-2017/introduction.tex

@@ -55 +55 @@
 Since 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.
 
-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.
-
-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}.
+In 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.
+
+We 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}.
 To 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.
 
@@ -136 +136 @@
 decouple execution time from execution history by introducing randomisation.
 
-In CerCo~\cite{cerco} we do not address this problem, optimistically assuming
+In CerCo we do not address this problem, optimistically assuming
 that improvements in low-level timing analysis or architecture will make
 verification feasible in the longer term.