Changeset 551


Ignore:
Timestamp:
Feb 17, 2011, 1:04:15 PM (6 years ago)
Author:
mulligan
Message:

more added to bibliography

Location:
Deliverables/D4.1/ITP-Paper
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.bib

    r550 r551  
    4444
    4545@inproceedings
     46{ chlipala:verified:2010,
     47  author = {Adam Chlipala},
     48  title = {A verified compiler for an impure functional language},
     49  booktitle = {Proceedings of the Thirty Seventh Annual Symposium on Principles of Programming Languages {(POPL 2010)}},
     50  series = {{ACM SIGPLAN} Notices},
     51  volume = {45},
     52  issue = {1},
     53  pages = {93--106},
     54  year = {2010}
     55}
     56
     57@inproceedings
    4658{ fox:trustworthy:2010,
    4759  author = {Anthony Fox and Magnus O. Myreen},
     
    6678
    6779@misc
     80{ cerco:2011,
     81  title = {The {CerCo} {FeT-Open} Project},
     82  howpublished = {\url{http://cerco.cs.unibo.it}},
     83  year = {2011},
     84  key = {{CerCo}}
     85}
     86
     87@misc
    6888{ mcu8051ide:2010,
    6989  title = {{MCU 8051 IDE} 1.3.11},
     
    80100  key = {{SDCC}}
    81101}
     102
     103@techreport
     104{ amadio:certifying:2010,
     105  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
     106  title = {Cerifying cost annotations in compilers},
     107  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
     108  year = {2010}
     109}
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r550 r551  
    8888
    8989Formal methods are designed to increase our confidence in the design and implementation of software (and hardware).
    90 Ideally, we would like all software to come equipped with a formal specification, along with a proof of correctness for the implementation.
    91 Today practically all programs are written in high level languages and then compiled into low level ones.
     90Ideally, we would like all software to come equipped with a formal specification, along with a proof of correctness that the software meets this specification.
     91Today the majority of programs are written in high level languages and then compiled into low level ones.
    9292Specifications are therefore also given at a high level and correctness can be proved by reasoning automatically or interactively on the program's source code.
    9393The code that is actually run, however, is not the high level source code that we reason on, but the object code that is generated by the compiler.
    94 
    9594A few simple questions now arise:
    9695\begin{itemize*}
     
    102101To what extent can you trust your compiler in preserving those properties?
    103102\end{itemize*}
    104 These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification}.
     103These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification} (for instance~\cite{leroy:formal:2009, chlipala:verified:2010}, and many others).
    105104So far, the field has been focused on the first and last questions only.
    106105In particular, much attention has been placed on verifying compiler correctness with respect to extensional properties of programs, which are easily preserved during compilation; it is sufficient to completely preserve the denotational semantics of the input program.
     
    112111Therefore both the cost model and intensional specifications are affected by the compilation process.
    113112
    114 In the current EU project CerCo (`Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows.
     113In the current EU project CerCo (`Certified Complexity')~\cite{cerco:2011} we approach the problem of reasoning about intensional properties of programs as follows.
    115114We are currently developing a compiler that induces a cost model on the high level source code.
    116115Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled object code.
     
    118117However, the model has the potential to be extremely \emph{precise}, capturing a program's \emph{realistic} cost, by taking into account, not ignoring, the compilation process.
    119118A prototype compiler, where no approximation of the cost is provided, has been developed.
     119(The full technical details of the CerCo cost model is explained in~\cite{amadio:certifying:2010}.)
    120120
    121121We believe that our approach is especially applicable to certifying real time programs.
Note: See TracChangeset for help on using the changeset viewer.