Ignore:
Timestamp:
Mar 7, 2017, 11:04:27 AM (3 years ago)
Author:
mulligan
Message:

Small tweaks before work on another paper

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/conclusions.tex

    r3630 r3632  
    4141
    4242\paragraph{Compiler-based cost-model lifting}
    43 Perhaps the most similar piece of work to our own is the recent work by Carbonneaux \emph{et al}, who extended the CompCert verified C compiler in order to lift a concrete cost model for stack space usage back to the C source-level.
     43Perhaps the most similar piece of work to our own is the recent work by Carbonneaux \emph{et al}~\cite{DBLP:conf/pldi/Carbonneaux0RS14}, who extended the CompCert verified C compiler in order to lift a concrete cost model for stack space usage back to the C source-level.
    4444Like CerCo, this work was verified within a theorem prover---in this case Coq, rather than Matita.
    4545Though Carbonneaux \emph{et al} were working entirely independently of the project described herein\footnote{Personal communication with Carbonneaux and Hoffmann}, the two pieces of work share some remarkable similarities, with both projects developing an analogue of the `structured trace' data structure described earlier in this paper in order to facilitate the verification of the lifting.
    4646However, differences between the two projects exist.
    47 Carbonneaux \emph{et al} developed a `quantitative' Hoare logic for manually reasoning about stack space usage of compiled programs; we developed a FramaC plugin for automatically establishing resource bounds, modulo a degree of user input.
     47Carbonneaux \emph{et al} developed a `quantitative' Hoare logic for manually reasoning about stack space usage of compiled programs, coupled with an automated stack-space usage analyser built at the Clight intermediate language level; we developed a FramaC plugin for automatically establishing resource bounds, from the parametric complexity analysis offered by our compiler, modulo a degree of user input.
    4848Carbonneaux \emph{at al} lift a cost model for stack space usage; we lift a cost model for time and stack space usage.
    4949Carbonneaux \emph{at al} lift their model from the assembly generated by the CompCert compiler; we must go further, to the level of machine code, in order to lift our timing cost model, necessitating the development of a verified assembler.
    50 Nevertheless, despite the differences, the two projects are clearly closely related.
     50Nevertheless, despite these differences, the two projects are clearly closely related.
    5151
    5252\paragraph{WCET, and Abstract Interpretation}
Note: See TracChangeset for help on using the changeset viewer.