# Changeset 3632

Ignore:
Timestamp:
Mar 7, 2017, 11:04:27 AM (8 months ago)
Message:

Small tweaks before work on another paper

Location:
Papers/jar-cerco-2017
Files:
2 edited

### Legend:

Unmodified
 r3630 \paragraph{Compiler-based cost-model lifting} 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. Perhaps 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. Like CerCo, this work was verified within a theorem prover---in this case Coq, rather than Matita. Though 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. However, differences between the two projects exist. 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. Carbonneaux \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. Carbonneaux \emph{at al} lift a cost model for stack space usage; we lift a cost model for time and stack space usage. Carbonneaux \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. Nevertheless, despite the differences, the two projects are clearly closely related. Nevertheless, despite these differences, the two projects are clearly closely related. \paragraph{WCET, and Abstract Interpretation}