# Changeset 1775 for Deliverables/D1.2/CompilerProofOutline

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

...

File:
1 edited

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

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