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

Last change on this file since 555 was 555, checked in by mulligan, 8 years ago

Resolved conflict, updated bibtex, finished bibliography, and llncs.cls updated to latest version.

File size: 4.8 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 Fourteenth {IEEE} Symposium on Real-time and Embedded Technology and Applications ({RTAS 2008})},
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 {(TYPES 2007)}},
48  pages = {18--32},
49  series = {Lecture Noted in Computer Science},
50  volume = {4941},
51  year = {2007}
52}
53
54@inproceedings
55{ blazy:formal:2006,
56  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
57  title = {Formal Verification of a {C} Compiler Front-End},
58  booktitle = {Proceedings of the International Symposium on Formal Methods ({FM 2006})},
59  series = {Lecture Notes in Computer Science},
60  volume = {4085},
61  pages = {460--475},
62  year = {2006}
63}
64
65@inproceedings
66{ chlipala:verified:2010,
67  author = {Adam Chlipala},
68  title = {A verified compiler for an impure functional language},
69  booktitle = {Proceedings of the Thirty Seventh Annual Symposium on Principles of Programming Languages {(POPL 2010)}},
70  series = {{ACM SIGPLAN} Notices},
71  volume = {45},
72  issue = {1},
73  pages = {93--106},
74  year = {2010}
75}
76
77@inproceedings
78{ fox:trustworthy:2010,
79  author = {Anthony Fox and Magnus O. Myreen},
80  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
81  booktitle = {Proceedings of the First International Conference on Interactive Theorem Proving ({ITP 2010})},
82  series = {Lecture Notes in Computer Science},
83  pages = {243--258},
84  year = {2010}
85}
86
87@inproceedings
88{ garrigue:programming:1998,
89  author = {Jacques Garrigue},
90  title = {Programming with polymorphic variants},
91  booktitle = {The {ML} Workshop},
92  year = {1998}
93}
94
95@inproceedings
96{ leijen:domain:1999,
97  author = {Daan Leijen and Erik Meijer},
98  title = {Domain specific embedded compilers},
99  booktitle = {Proceedings of the Second Conference on Domain Specific Languages {(DSL 1999)}},
100  series = {{ACM SIGPLAN} Notices},
101  pages = {109--122},
102  volume = {2},
103  year = {1999}
104}
105
106@inproceedings
107{ sarkar:semantics:2009,
108  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},
109  title = {The semantics of {x86-CC} multiprocessor machine code},
110  booktitle = {Proceedings of the Thirty Sixth Annual Symposium on Principles of Programming Languages {(POPL 2009)}},
111  series = {{ACM SIGPLAN} Notices},
112  pages = {379--391},
113  volume = {44},
114  issue = {1},
115  year = {2009}
116}
117
118@misc
119{ cerco:2011,
120  title = {The {CerCo} {FeT-Open} Project},
121  howpublished = {\url{http://cerco.cs.unibo.it}},
122  year = {2011},
123  key = {{CerCo}}
124}
125
126@misc
127{ mcu8051ide:2010,
128  title = {{MCU 8051 IDE} 1.3.11},
129  howpublished = {\url{http://mcu8051ide.sourceforge.net/}},
130  year = {2010},
131  key = {{MCU}}
132}
133
134@misc
135{ oliboni:matita:2008,
136  author = {Cosimo A. Oliboni},
137  title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}},
138  institution = {Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna},
139  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
140  year = {2008}
141}
142
143@misc
144{ sdcc:2010,
145  title = {Small Device {C} Compiler {(SDCC)} 3.0.0},
146  howpublished = {\url{http://sdcc.sourceforge.net/}},
147  year = {2010},
148  key = {{SDCC}}
149}
150
151@misc
152{ siemens:2011,
153  title = {Siemens Semiconductor Group 8051 derivative instruction set},
154  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
155  year = {2011},
156  key = {{Siemens}}
157}
158
159@techreport
160{ amadio:certifying:2010,
161  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
162  title = {Cerifying cost annotations in compilers},
163  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
164  year = {2010}
165}
Note: See TracBrowser for help on using the repository browser.