Ignore:
Timestamp:
Feb 6, 2013, 9:32:13 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec.tex

    r2625 r2626  
    895895
    896896\begin{condition}[Case \texttt{cl\_return}]
    897  For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
    898  $\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
    899 $(\texttt{trace\_any\_any}~s_2~s_b)$, a $taaf$ of type
    900 $(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
     897 For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$,
     898 $\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
     899$\texttt{trace\_any\_any}~s_2~s_b$, a
     900$\texttt{trace\_any\_any\_free}~s_a~s_2'$ called $taaf$ such that:
    901901$s_a$ is classified as a \texttt{cl\_return},
    902902$s_1 \mathcal{C} s_b$, the predicate
    903 $(\texttt{as\_execute}~s_b~s_a)$ holds,
     903$\texttt{as\_execute}~s_b~s_a$ holds,
    904904$s_1' \mathcal{R} s_a$ and
    905905$s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
     
    10651065of a traditional, function properties only, proof.
    10661066
    1067 All the results presented in the paper are part of a larger certification of a
     1067All results presented in the paper are part of a larger certification of a
    10681068C compiler which is based on the labelling approach. The certification, done
    1069 in Matita, is the main deliverable of the European Project CerCo.
     1069in Matita, is the main deliverable of the FET-Open Certified Complexity (CerCo).
    10701070
    10711071The short term future work consists in the completion of the certification of
     
    10891089function constitutes then a cost model for the source code, in the spirit of
    10901090what we are doing in CerCo. However, we believe our solution to be superior
    1091 in the following points: 1) the machinery of the labelling approach is
     1091in the following respects: 1) the machinery of the labelling approach is
    10921092insensible to the resource being measured. Indeed, any cost model computed on
    10931093the object code can be lifted to the source code (e.g. stack space used,
     
    11001100models can be induced when the approach is scaled to cover, for instance,
    11011101loop optimizations~\cite{loopoptimizations}, but the costs are still meant to
    1102 be easy to understandable and manipulate in an interactive theorem prover.
     1102be easy to understand and manipulate in an interactive theorem prover or
     1103in Frama-C.
    11031104On the contrary, a clock function is a complex function of the state $s_1$
    11041105which, as a function, is an opaque object that is difficult to reify as
Note: See TracChangeset for help on using the changeset viewer.