Index: Papers/itp-2013/ccexec.bib
===================================================================
--- Papers/itp-2013/ccexec.bib (revision 2625)
+++ Papers/itp-2013/ccexec.bib (revision 2626)
@@ -413,9 +413,9 @@
INIauthor = {R. Amadio and A. Asperti and N. Ayache and
B. Campbell and D. Mulligan and R. Pollack and
- Y. R{\'e}gis-Gianas and C. Sacerdoti Coen and I.
+ Y. R{\'e}gis-Gianas and C. {Sacerdoti Coen} and I.
Stark},
author = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
Brian Campbell and Dominic Mulligan and Randy Pollack and
- Yann R{\'e}gis-Gianas and Claudio Sacerdoti Coen and Ian
+ Yann R{\'e}gis-Gianas and Claudio {Sacerdoti Coen} and Ian
Stark},
title = {Certified Complexity},
Index: Papers/itp-2013/ccexec.tex
===================================================================
--- Papers/itp-2013/ccexec.tex (revision 2625)
+++ Papers/itp-2013/ccexec.tex (revision 2626)
@@ -895,11 +895,11 @@
\begin{condition}[Case \texttt{cl\_return}]
- For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
- $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_return}$, there exists $s_2', s_b, s_a$, a $taa$ of type
-$(\texttt{trace\_any\_any}~s_2~s_b)$, a $taaf$ of type
-$(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
+ For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$,
+ $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_return}$, there exists $s_2', s_b, s_a$, a
+$\texttt{trace\_any\_any}~s_2~s_b$, a
+$\texttt{trace\_any\_any\_free}~s_a~s_2'$ called $taaf$ such that:
$s_a$ is classified as a \texttt{cl\_return},
$s_1 \mathcal{C} s_b$, the predicate
-$(\texttt{as\_execute}~s_b~s_a)$ holds,
+$\texttt{as\_execute}~s_b~s_a$ holds,
$s_1' \mathcal{R} s_a$ and
$s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
@@ -1065,7 +1065,7 @@
of a traditional, function properties only, proof.
-All the results presented in the paper are part of a larger certification of a
+All results presented in the paper are part of a larger certification of a
C compiler which is based on the labelling approach. The certification, done
-in Matita, is the main deliverable of the European Project CerCo.
+in Matita, is the main deliverable of the FET-Open Certified Complexity (CerCo).
The short term future work consists in the completion of the certification of
@@ -1089,5 +1089,5 @@
function constitutes then a cost model for the source code, in the spirit of
what we are doing in CerCo. However, we believe our solution to be superior
-in the following points: 1) the machinery of the labelling approach is
+in the following respects: 1) the machinery of the labelling approach is
insensible to the resource being measured. Indeed, any cost model computed on
the object code can be lifted to the source code (e.g. stack space used,
@@ -1100,5 +1100,6 @@
models can be induced when the approach is scaled to cover, for instance,
loop optimizations~\cite{loopoptimizations}, but the costs are still meant to
-be easy to understandable and manipulate in an interactive theorem prover.
+be easy to understand and manipulate in an interactive theorem prover or
+in Frama-C.
On the contrary, a clock function is a complex function of the state $s_1$
which, as a function, is an opaque object that is difficult to reify as