Changeset 2609


Ignore:
Timestamp:
Feb 6, 2013, 1:56:01 PM (6 years ago)
Author:
sacerdot
Message:

Bibliography in place.

Location:
Papers/itp-2013
Files:
1 added
1 edited

Legend:

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

    r2607 r2609  
    9393architectures and caches.
    9494
    95 In the European Project CerCo (Certified Complexity~\footnote{\url{http://cerco.cs.unibo.it}}) we are certifying a labelling approach based compiler for a large subset of C to
     95In the European Project CerCo (Certified Complexity~\footnote{\url{http://cerco.cs.unibo.it}})~\cite{cerco} we are certifying a labelling approach based compiler for a large subset of C to
    96968051 object code. The compiler is
    9797moderately optimizing and implements a compilation chain that is largely
    98 inspired to that of CompCert~\cite{compcert}. Compared to work done in~\cite{easylabelling}, the main novely and source of difficulties is due to the presence
     98inspired to that of CompCert~\cite{compcert1,compcert2}. Compared to work done in~\cite{easylabelling}, the main novely and source of difficulties is due to the presence
    9999of function calls. Surprisingly, the addition of function calls require a
    100100rivisitation of the proof technique given in~\cite{easylabelling}. In
     
    172172This correctness property is called in the litterature a forward simulation
    173173and is sufficient for correctness when the target language is
    174 deterministic~\cite{leroy}.
     174deterministic~\cite{compcert3}.
    175175We also require a stronger, non-functional preservation property: after each
    176176pass all basic blocks must start with an emission statement, and all labels
     
    890890precise cost model on the source code in order to establish non-functional
    891891properties of programs on an high level language. Traditional certifications
    892 of compilers, like~\cite{compcert,python}, only explicitly prove preservation
     892of compilers, like~\cite{compcert2,piton}, only explicitly prove preservation
    893893of the functional properties via forward simulations.
    894894
Note: See TracChangeset for help on using the changeset viewer.