# Changeset 3625

Ignore:
Timestamp:
Mar 6, 2017, 5:20:48 PM (10 months ago)
Message:

more work on related work section

File:
1 edited

### Legend:

Unmodified
 r3624 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 mannually reasoning about stack space usage of compiled programs; we developed a FramaC plugin for automatically establishing resource bounds, modulo a degree of user input. Carbo 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{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, the two projects are clearly closely related, and similar in spirit, and in our view the existence of two projects stumbling upon similar approaches demonstrates the naturality of the techniques developed by both. \subsection{Further work}