Changeset 551 for Deliverables

Timestamp:

Feb 17, 2011, 1:04:15 PM (11 years ago)

Author:

mulligan

Message:

more added to bibliography

Location:

Deliverables/D4.1/ITP-Paper

Files:

• itp-2011.bib (modified) (3 diffs)
• itp-2011.tex (modified) (4 diffs)

Deliverables/D4.1/ITP-Paper/itp-2011.bib

@@ -44 +44 @@
 
 @inproceedings
+{ chlipala:verified:2010,
+  author = {Adam Chlipala},
+  title = {A verified compiler for an impure functional language},
+  booktitle = {Proceedings of the Thirty Seventh Annual Symposium on Principles of Programming Languages {(POPL 2010)}},
+  series = {{ACM SIGPLAN} Notices},
+  volume = {45},
+  issue = {1},
+  pages = {93--106},
+  year = {2010}
+}
+
+@inproceedings
 { fox:trustworthy:2010,
   author = {Anthony Fox and Magnus O. Myreen},
@@ -66 +78 @@
 
 @misc
+{ cerco:2011,
+  title = {The {CerCo} {FeT-Open} Project},
+  howpublished = {\url{http://cerco.cs.unibo.it}},
+  year = {2011},
+  key = {{CerCo}}
+}
+
+@misc
 { mcu8051ide:2010,
   title = {{MCU 8051 IDE} 1.3.11},
@@ -80 +100 @@
   key = {{SDCC}}
 }
+
+@techreport
+{ amadio:certifying:2010,
+  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
+  title = {Cerifying cost annotations in compilers},
+  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
+  year = {2010}
+}

Deliverables/D4.1/ITP-Paper/itp-2011.tex

@@ -88 +88 @@
 
 Formal methods are designed to increase our confidence in the design and implementation of software (and hardware).
-Ideally, we would like all software to come equipped with a formal specification, along with a proof of correctness for the implementation.
-Today practically all programs are written in high level languages and then compiled into low level ones.
+Ideally, we would like all software to come equipped with a formal specification, along with a proof of correctness that the software meets this specification.
+Today the majority of programs are written in high level languages and then compiled into low level ones.
 Specifications are therefore also given at a high level and correctness can be proved by reasoning automatically or interactively on the program's source code.
 The 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.
-
 A few simple questions now arise:
 \begin{itemize*}
@@ -102 +101 @@
 To what extent can you trust your compiler in preserving those properties?
 \end{itemize*}
-These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification}.
+These 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).
 So far, the field has been focused on the first and last questions only.
 In 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.
@@ -112 +111 @@
 Therefore both the cost model and intensional specifications are affected by the compilation process.
 
-In the current EU project CerCo (`Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows.
+In the current EU project CerCo (`Certified Complexity')~\cite{cerco:2011} we approach the problem of reasoning about intensional properties of programs as follows.
 We are currently developing a compiler that induces a cost model on the high level source code.
 Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled object code.
@@ -118 +117 @@
 However, 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.
 A prototype compiler, where no approximation of the cost is provided, has been developed.
+(The full technical details of the CerCo cost model is explained in~\cite{amadio:certifying:2010}.)
 
 We believe that our approach is especially applicable to certifying real time programs.