Ignore:
Timestamp:
Feb 27, 2012, 4:11:48 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1774 r1775  
    997997the CompCert project~\cite{compcert} for the CompCert pass that is closest to
    998998ours; 3) an estimation of the complexity of the pass according to the
    999 analysis above.
    1000 
     999analysis above. The result is shown in Table~\ref{table}.
     1000
     1001\begin{table}{h}
    10011002\begin{tabular}{lrlrr}
    10021003Pass origin & Code lines & CompCert ratio & Estimated effort & Estimated effort \\
     
    10191020Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
    10201021\end{tabular}
     1022\caption{\label{table}Estimated effort}
     1023\end{table}
    10211024
    10221025We provide now some additional informations on the methodology used in the
     
    10871090less than 1/3rd of the total effort. At least half of this effort really goes
    10881091into simple data structures (vectors, bounded and unbounded integers, tries
    1089 and maps) whose certification is not very interesting and could be sacrificed.
     1092and maps) whose certification is not interesting and whose code could be
     1093taken without re-proving it from the library of any other theorem prover.
    10901094
    10911095\section{Conclusions}
Note: See TracChangeset for help on using the changeset viewer.