Changeset 3625


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

more work on related work section

File:
1 edited

Legend:

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

    r3624 r3625  
    5151Though 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.
    5252However, differences between the two projects exist.
    53 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.
    54 Carbo
     53Carbonneaux \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.
     54Carbonneaux \emph{at al} lift a cost model for stack space usage; we lift a cost model for time and stack space usage.
     55Carbonneaux \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.
     56Nevertheless, 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.
    5557
    5658\subsection{Further work}
Note: See TracChangeset for help on using the changeset viewer.