source: Deliverables/addenda/indexed_labels/bib.bib @ 1673

Last change on this file since 1673 was 1673, checked in by tranquil, 7 years ago

report on indexed labels
TODO: corrections, examples, etc

File size: 4.0 KB
Line 
1% LaTeX definitions
2@Preamble{"\newcommand{\online}[1]{Available at \url{#1}}"}
3
4
5%% hal-00524715, version 1
6%% http://hal.archives-ouvertes.fr/hal-00524715
7@unpublished{D2.1,
8    hal_id = {hal-00524715},
9    note = {Deliverable 2.1 of Project FP7-ICT-2009-C-243881 CerCo, \online{http://hal.archives-ouvertes.fr/hal-00524715}},
10    title = {{Certifying cost annotations in compilers}},
11    author = {Amadio, Roberto M. and Ayache, Nicolas and R{\'e}gis-Gianas, Yann and Saillard, Ronan},
12    abstract = {{We discuss the problem of building a compiler which can lift in a provably correct way pieces of information on the execution cost of the object code to cost annotations on the source code. To this end, we need a clear and flexible picture of: (i) the meaning of cost annotations, (ii) the method to prove them sound and precise, and (iii) the way such proofs can be composed. We propose a so-called labelling approach to these three questions. As a first step, we examine its application to a toy compiler. This formal study suggests that the labelling approach has good compositionality and scalability properties. In order to provide further evidence for this claim, 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.}},
13    keywords = {Certified compilation. Worst case execution time.},
14    language = {Anglais},
15    affiliation = {Preuves, Programmes et Syst{\`e}mes - PPS , PI.R2 - INRIA Paris - Rocquencourt},
16    pdf = {http://hal.archives-ouvertes.fr/hal-00524715/PDF/ccac-hal.pdf}
17}
18
19@unpublished{D2.2,
20    note = {Deliverable 2.2 of Project FP7-ICT-2009-C-243881 CerCo, \online{http://cerco.cs.unibo.it/}},
21    title = {Prototype implementation},
22    author = {Amadio, Roberto M. and Ayache, Nicolas and R{\'e}gis-Gianas, Yann and Saillard, Ronan},
23    keywords = {Certified compilation. Worst case execution time.},
24    language = {Anglais},
25    affiliation = {Preuves, Programmes et Syst{\`e}mes - PPS , PI.R2 - INRIA Paris - Rocquencourt}
26}
27
28@Misc{absint,
29title = {AbsInt Angewandte Informatik},
30note = {\url{http://www.absint.com/}},
31url = {http://www.absint.com/}
32}
33
34@Misc{framac,
35title = {Frama-C software analyzers},
36note = {\url{http://frama-c.com/}},
37url = {http://frama-c.com/}
38}
39
40@book{muchnick,
41  author    = {Steven S. Muchnick},
42  title     = {Advanced Compiler Design and Implementation},
43  publisher = {Morgan Kaufmann},
44  year      = {1997},
45  isbn      = {1-55860-320-4},
46  bibsource = {DBLP, http://dblp.uni-trier.de}
47}
48
49@BOOK{morgan,
50  author = {Robert Morgan},
51  title = {Building an Optimizing Compiler},
52  publisher = {Digital Press},
53  year = {1998},
54  abstract = {out of print}
55}
56
57@article{PRE,
58 author = {Morel, E. and Renvoise, C.},
59 title = {Global optimization by suppression of partial redundancies},
60 journal = {Commun. ACM},
61 volume = {22},
62 issue = {2},
63 month = {February},
64 year = {1979},
65 issn = {0001-0782},
66 pages = {96--103},
67 numpages = {8},
68 url = {http://doi.acm.org/10.1145/359060.359069},
69 doi = {http://doi.acm.org/10.1145/359060.359069},
70 acmid = {359069},
71 publisher = {ACM},
72 address = {New York, NY, USA},
73 keywords = {Boolean systems, compilation, compiler, data flow analysis, invariant computation elimination, optimization, optimizer, partial redundancy, redundancy elimination},
74}
75
76@article{cacheprediction,
77 author = {Ferdinand, Christian and Wilhelm, Reinhard},
78 title = {Efficient and Precise Cache Behavior Prediction for Real-TimeSystems},
79 journal = {Real-Time Syst.},
80 volume = {17},
81 issue = {2-3},
82 month = {December},
83 year = {1999},
84 issn = {0922-6443},
85 pages = {131--181},
86 numpages = {51},
87 url = {http://dx.doi.org/10.1023/A:1008186323068},
88 doi = {http://dx.doi.org/10.1023/A:1008186323068},
89 acmid = {338858},
90 publisher = {Kluwer Academic Publishers},
91 address = {Norwell, MA, USA},
92 keywords = {abstract interpretation, cache behavior prediction, cache memories, program analysis, real time applications, worst case execution time prediction},
93}
94
Note: See TracBrowser for help on using the repository browser.