Changeset 3632


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

Small tweaks before work on another paper

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

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.bib

    r3623 r3632  
    44 institution = {Technische Universit\"at Wien},
    55 year = {2005}
     6}
     7
     8@inproceedings{DBLP:conf/pldi/Carbonneaux0RS14,
     9  author    = {Quentin Carbonneaux and
     10               Jan Hoffmann and
     11               Tahina Ramananandro and
     12               Zhong Shao},
     13  title     = {End-to-end verification of stack-space bounds for {C} programs},
     14  booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
     15               {PLDI} '14, Edinburgh, United Kingdom - June 09 - 11, 2014},
     16  pages     = {270--281},
     17  year      = {2014},
     18  crossref  = {DBLP:conf/pldi/2014},
     19  url       = {http://doi.acm.org/10.1145/2594291.2594301},
     20  doi       = {10.1145/2594291.2594301},
     21  timestamp = {Tue, 20 Dec 2016 10:12:01 +0100},
     22  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/pldi/Carbonneaux0RS14},
     23  bibsource = {dblp computer science bibliography, http://dblp.org}
    624}
    725
  • 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.