Changeset 551 for Deliverables
- Timestamp:
- Feb 17, 2011, 1:04:15 PM (10 years ago)
- Location:
- Deliverables/D4.1/ITP-Paper
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.bib
r550 r551 44 44 45 45 @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 46 58 { fox:trustworthy:2010, 47 59 author = {Anthony Fox and Magnus O. Myreen}, … … 66 78 67 79 @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 68 88 { mcu8051ide:2010, 69 89 title = {{MCU 8051 IDE} 1.3.11}, … … 80 100 key = {{SDCC}} 81 101 } 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 88 88 89 89 Formal 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 allprograms are written in high level languages and then compiled into low level ones.90 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. 91 Today the majority of programs are written in high level languages and then compiled into low level ones. 92 92 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. 93 93 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. 94 95 94 A few simple questions now arise: 96 95 \begin{itemize*} … … 102 101 To what extent can you trust your compiler in preserving those properties? 103 102 \end{itemize*} 104 These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification} .103 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). 105 104 So far, the field has been focused on the first and last questions only. 106 105 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. 113 112 114 In the current EU project CerCo (`Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows.113 In the current EU project CerCo (`Certified Complexity')~\cite{cerco:2011} we approach the problem of reasoning about intensional properties of programs as follows. 115 114 We are currently developing a compiler that induces a cost model on the high level source code. 116 115 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. 119 118 A 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}.) 120 120 121 121 We believe that our approach is especially applicable to certifying real time programs.
Note: See TracChangeset
for help on using the changeset viewer.