source: Deliverables/D3.4/Report/report.bib

Last change on this file was 3231, checked in by campbell, 7 years ago

Final revisions to 3.4.

File size: 5.4 KB
Line 
1
2@misc{d2.1,
3title = {Compiler design and intermediate languages},
4author = {Roberto M. Amadio and Nicolas Ayache and Yann R{\'{e}}gis-Gianas and Kayvan Memarian and Ronan Saillard},
5howpublished = {Deliverable 2.1, Project FP7-ICT-2009-C-243881 CerCo},
6}
7
8@misc{d2.2,
9title = {Prototype implementation},
10author = {Nicolas Ayache and Roberto M. Amadio and Yann R{\'{e}}gis-Gianas},
11howpublished = {Deliverable 2.2, Project FP7-ICT-2009-C-243881 CerCo},
12}
13
14@misc{d3.1,
15title = {Executable Formal Semantics of {C}},
16author = {Brian Campbell and Randy Pollack},
17howpublished = {Deliverable 3.1, Project FP7-ICT-2009-C-243881 CerCo},
18}
19
20@misc{d3.2,
21title = {{CIC} encoding: Front-end},
22author = {Brian Campbell},
23howpublished = {Deliverable 3.2, Project FP7-ICT-2009-C-243881 CerCo},
24}
25
26@misc{d3.3,
27title = {Executable Formal Semantics of front-end intermediate languages},
28author = {Brian Campbell},
29howpublished = {Deliverable 3.3, Project FP7-ICT-2009-C-243881 CerCo},
30}
31
32@misc{d4.1,
33title = {Executable Formal Semantics of Machine Code},
34author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
35howpublished = {Deliverable 4.1, Project FP7-ICT-2009-C-243881 CerCo},
36}
37
38@misc{d4.2,
39title = {{CIC} encoding: Back-end},
40author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
41howpublished = {Deliverable 4.2, Project FP7-ICT-2009-C-243881 CerCo},
42}
43
44@misc{d4.3,
45title = {Executable formal semantics of back-end intermediate languages},
46author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
47howpublished = {Deliverable 4.3, Project FP7-ICT-2009-C-243881 CerCo},
48}
49
50@incollection {springerlink:10.1007/978-3-642-32469-7_3,
51   author = {Ayache, Nicolas and Amadio, Roberto and R{\'{e}}gis-Gianas, Yann},
52   affiliation = {Universit{\'{e}} Paris Diderot (UMR-CNRS 7126), France},
53   title = {Certifying and Reasoning on Cost Annotations in {C} Programs},
54   booktitle = {Formal Methods for Industrial Critical Systems},
55   series = {Lecture Notes in Computer Science},
56   editor = {Stoelinga, Mari{\"{e}}lle and Pinger, Ralf},
57   publisher = {Springer Berlin / Heidelberg},
58   isbn = {978-3-642-32468-0},
59   keyword = {Computer Science},
60   pages = {32-46},
61   volume = 7437,
62   url = {http://dx.doi.org/10.1007/978-3-642-32469-7_3},
63   note = {10.1007/978-3-642-32469-7\_3},
64   abstract = {We present a so-called labelling method to enrich a compiler in order to turn it into a “cost annotating compiler”, that is, a compiler which can lift pieces of information on the execution cost of the object code as cost annotations on the source code. These cost annotations characterize the execution costs of code fragments of constant complexity. The first contribution of this paper is a proof methodology that extends standard simulation proofs of compiler correctness to ensure that the cost annotations on the source code are sound and precise with respect to an execution cost model of the object code. As a second contribution, we demonstrate that our label-based instrumentation is scalable because it consists in a modular extension of the compilation chain. To that end, we report our successful experience in implementing and testing the labelling approach on top of a prototype compiler written in ocaml for (a large fragment of) the C language. As a third and last contribution, we provide evidence for the usability of the generated cost annotations as a mean to reason on the concrete complexity of programs written in C . For this purpose, we present a Frama-C plugin that uses our cost annotating compiler to automatically infer trustworthy logic assertions about the concrete worst case execution cost of programs written in a fragment of the C language. These logic assertions are synthetic in the sense that they characterize the cost of executing the entire program, not only constant-time fragments. (These bounds may depend on the size of the input data.) We report our experimentations on some C programs, especially programs generated by a compiler for the synchronous programming language Lustre used in critical embedded software.},
65   year = 2012
66}
67
68@article{Leroy-backend,
69  author = {Xavier Leroy},
70  title = {A formally verified compiler back-end},
71  journal = {Journal of Automated Reasoning},
72  volume = 43,
73  number = 4,
74  pages = {363--446},
75  year = 2009,
76  url = {http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf},
77  urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
78  hal = {http://hal.inria.fr/inria-00360768/},
79  pubkind = {journal-int-mono}
80}
81
82@article{Blazy-Leroy-Clight-09,
83  author = {Sandrine Blazy and Xavier Leroy},
84  title = {Mechanized semantics for the {Clight}
85                         subset of the {C} language},
86  year = 2009,
87  journal = {Journal of Automated Reasoning},
88  url = {http://gallium.inria.fr/~xleroy/publi/Clight.pdf},
89  hal = {http://hal.inria.fr/inria-00352524/},
90  urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9148-3},
91  volume = 43,
92  number = 3,
93  pages = {263-288}
94}
95
96@article{2008-Leroy-Blazy-memory-model,
97  author = {Xavier Leroy and Sandrine Blazy},
98  title = {Formal verification of a {C}-like memory model
99                 and its uses for verifying program transformations},
100  journal = {Journal of Automated Reasoning},
101  volume = 41,
102  number = 1,
103  pages = {1--31},
104  url = {http://gallium.inria.fr/~xleroy/publi/memory-model-journal.pdf},
105  urlpublisher = {http://dx.doi.org/10.1007/s10817-008-9099-0},
106  hal = {http://hal.inria.fr/inria-00289542/},
107  year = 2008,
108  pubkind = {journal-int-multi}
109}
Note: See TracBrowser for help on using the repository browser.