source: Deliverables/D4.1/ITP-Paper/itp-2011.bib @ 571

Last change on this file since 571 was 571, checked in by mulligan, 10 years ago

Finished tightening everything up. Just under 16 pages. Cannot add another sentence without it going over!

File size: 5.0 KB
Line 
1@article
2{ bate:wcet:2011,
3  author = {Iain Bate and Usman Khan},
4  title = {{WCET} analysis of modern processors using multi-criteria optimisation},
5  journal = {Empirical Software Engineering},
6  pages = {5--28},
7  volume = {16},
8  issue = {1},
9  year = {2011}
10}
11
12@article
13{ leroy:formal:2009,
14  author = {Xavier Leroy},
15  title = {Formal verification of a realistic compiler},
16  journal = {Communications of the {Association of Computing Machinery}},
17  volume = {52},
18  number = {7},
19  pages = {107--115},
20  year = {2009}
21}
22
23@article
24{ leroy:formally:2009,
25  author = {Xavier Leroy},
26  title = {A formally verified compiler back-end},
27  journal = {Journal of Automated Reasoning},
28  volume = {43},
29  number = {4},
30  pages = {363--446},
31  year = {2009}
32}
33
34@inproceedings
35{ yan:wcet:2008,
36  author = {Jun Yan and Wei Zhang},
37  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
38  booktitle = {Proceedings of the $\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
39  pages = {80--89},
40  year = {2008}
41}
42
43@inproceedings
44{ atkey:coqjvm:2007,
45  author = {Robert Atkey},
46  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
47  booktitle = {Proceedings of the Conference of the {TYPES} Project},
48  pages = {18--32},
49  year = {2007}
50}
51
52@inproceedings
53{ blazy:formal:2006,
54  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
55  title = {Formal Verification of a {C} Compiler Front-End},
56  booktitle = {Proceedings of the International Symposium on Formal Methods},
57  pages = {460--475},
58  year = {2006}
59}
60
61@inproceedings
62{ chlipala:verified:2010,
63  author = {Adam Chlipala},
64  title = {A verified compiler for an impure functional language},
65  booktitle = {Proceedings of the $\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},
66  pages = {93--106},
67  year = {2010}
68}
69
70@inproceedings
71{ fox:trustworthy:2010,
72  author = {Anthony Fox and Magnus O. Myreen},
73  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
74  booktitle = {Proceedings of the $\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
75  pages = {243--258},
76  year = {2010}
77}
78
79@inproceedings
80{ garrigue:programming:1998,
81  author = {Jacques Garrigue},
82  title = {Programming with polymorphic variants},
83  booktitle = {The {ML} Workshop},
84  year = {1998}
85}
86
87@inproceedings
88{ leijen:domain:1999,
89  author = {Daan Leijen and Erik Meijer},
90  title = {Domain specific embedded compilers},
91  booktitle = {Proceedings of the $\mathrm{2^{nd}}$ Conference on Domain Specific Languages},
92  pages = {109--122},
93  year = {1999}
94}
95
96@inproceedings
97{ sarkar:semantics:2009,
98  author = {Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and Jade Alglave},
99  title = {The semantics of {x86-CC} multiprocessor machine code},
100  booktitle = {Proceedings of the $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
101  pages = {379--391},
102  year = {2009}
103}
104
105@inproceedings
106{ shankar:principles:1999,
107  author = {Natarajan Shankar and Sam Owre},
108  title = {Principles and Pragmatics of Subtyping in {PVS}},
109  booktitle = {Recent Trends in Algebraic Development Techniques},
110  pages = {37--52},
111  year = {1999}
112}
113
114@inproceedings
115{ sozeau:subset:2006,
116  author = {Matthieu Sozeau},
117  title = {Subset coercions in {Coq}},
118  booktitle = {Proceedings of the Conference of the {TYPES} Project},
119  pages = {237--252},
120  year = {2006}
121}
122
123@misc
124{ cerco:2011,
125  title = {The {CerCo} {FeT-Open} Project},
126  howpublished = {\url{http://cerco.cs.unibo.it}},
127  year = {2011},
128  key = {{CerCo}}
129}
130
131@misc
132{ cerco-report:2011,
133  title = {D4.1: executable formal semantics of machine code},
134  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf}},
135  year = {2011},
136  key = {{CerCo-report}}
137}
138
139@misc
140{ mcu8051ide:2010,
141  title = {{MCU 8051 IDE} 1.3.11},
142  howpublished = {\url{http://mcu8051ide.sourceforge.net/}},
143  year = {2010},
144  key = {{MCU}}
145}
146
147@misc
148{ oliboni:matita:2008,
149  author = {Cosimo A. Oliboni},
150  title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}},
151  institution = {Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna},
152  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
153  year = {2008}
154}
155
156@misc
157{ sdcc:2010,
158  title = {Small Device {C} Compiler {(SDCC)} 3.0.0},
159  howpublished = {\url{http://sdcc.sourceforge.net/}},
160  year = {2010},
161  key = {{SDCC}}
162}
163
164@misc
165{ siemens:2011,
166  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
167  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
168  year = {2011},
169  key = {{Siemens}}
170}
171
172@techreport
173{ amadio:certifying:2010,
174  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
175  title = {Cerifying cost annotations in compilers},
176  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
177  year = {2010}
178}
Note: See TracBrowser for help on using the repository browser.