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

Last change on this file since 574 was 571, checked in by mulligan, 9 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.