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

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

implemented referees comments

File size: 5.7 KB
RevLine 
[549]1@article
[579]2{ asperti:user:2007,
[1199]3  author = {A. Asperti and C. Sacerdoti Coen and E. Tassi and S. Zacchiroli},
[579]4  title = {User interaction with the {Matita} proof assistant},
[1199]5  journal = {Automated Reasoning},
[579]6  pages = {109--139},
7  volume = {39},
8  issue = {2},
9  year = {2007}
10}
11
12@article
[555]13{ bate:wcet:2011,
[1199]14  author = {I. Bate and U. Khan},
[555]15  title = {{WCET} analysis of modern processors using multi-criteria optimisation},
16  journal = {Empirical Software Engineering},
17  pages = {5--28},
18  volume = {16},
19  issue = {1},
20  year = {2011}
21}
22
23@article
[549]24{ leroy:formal:2009,
[1199]25  author = {X. Leroy},
[549]26  title = {Formal verification of a realistic compiler},
[1199]27  journal = {CACM},
[549]28  volume = {52},
29  number = {7},
30  pages = {107--115},
31  year = {2009}
32}
33
34@article
35{ leroy:formally:2009,
[1199]36  author = {X. Leroy},
[549]37  title = {A formally verified compiler back-end},
[1199]38  journal = {Automated Reasoning},
[549]39  volume = {43},
40  number = {4},
41  pages = {363--446},
42  year = {2009}
43}
44
[814]45@article
46{ luo:coercive:1999,
[1199]47  author = {Z. Luo},
[814]48  title = {Coercive subtyping},
[1199]49  journal = {Logic and Computation},
[814]50  volume = {9},
51  number = {1},
52  pages = {105--130},
53  year = {1999}
54}
55
[549]56@inproceedings
[1203]57{ myreen:extensible:2009,
58  author = {M. O. Myreen and K. Slind and Michael J. C. Gordon},
59  title = {Extensible proof-producing compilation},
60  booktitle = {CC},
61  volume = {5501},
62  pages = {2--16},
63  year = {2009}
64}
65
66@inproceedings
67{ hunt:verifying:2010,
68  author = {W. A. Hunt Jr.},
69  title = {Verifying {VIA Nano} microprocessor components},
70  booktitle = {FMCAD},
71  year = {2010}
72}
73
74@inproceedings
[555]75{ yan:wcet:2008,
[1199]76  author = {J. Yan and W. Zhang},
[555]77  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
[1199]78  booktitle = {{RTAS}},
[555]79  pages = {80--89},
80  year = {2008}
81}
82
83@inproceedings
[549]84{ atkey:coqjvm:2007,
[1199]85  author = {R. Atkey},
[571]86  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
[1199]87  booktitle = {{TYPES}},
[549]88  pages = {18--32},
89  year = {2007}
90}
91
92@inproceedings
[815]93{ blanqui:designing:2010,
94  title = {Designing a {CPU} model: from a pseudo-formal document to fast code},
[1199]95  author = {F. Blanqui and C. Helmstetter and V. Joloboff and J. Monin and X. Shi},
96  booktitle = {{RAPIDO}},
[815]97  year = {2010}
98}
99
100@inproceedings
[549]101{ blazy:formal:2006,
[1199]102  author = {S. Blazy and Z. Dargaye and X. Leroy},
[549]103  title = {Formal Verification of a {C} Compiler Front-End},
[1199]104  booktitle = {FM},
[549]105  pages = {460--475},
106  year = {2006}
107}
108
109@inproceedings
[551]110{ chlipala:verified:2010,
[1199]111  author = {A. Chlipala},
[551]112  title = {A verified compiler for an impure functional language},
[1199]113  booktitle = {POPL},
[551]114  pages = {93--106},
115  year = {2010}
116}
117
118@inproceedings
[549]119{ fox:trustworthy:2010,
[1199]120  author = {A. Fox and M. O. Myreen},
[549]121  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
[1199]122  booktitle = {ITP},
[549]123  pages = {243--258},
124  year = {2010}
125}
126
127@inproceedings
[555]128{ garrigue:programming:1998,
[1199]129  author = {J. Garrigue},
[555]130  title = {Programming with polymorphic variants},
[579]131  booktitle = {{ML} Workshop},
[555]132  year = {1998}
133}
134
135@inproceedings
136{ leijen:domain:1999,
[1199]137  author = {D. Leijen and E. Meijer},
[555]138  title = {Domain specific embedded compilers},
[1199]139  booktitle = {DSL},
[555]140  pages = {109--122},
141  year = {1999}
142}
143
144@inproceedings
[549]145{ sarkar:semantics:2009,
[1199]146  author = {S. Sarkar and P. Sewell and F. Zappa Nardelli and S. Owens and T. Ridge and T. Braibant and M. O. Myreen and J. Alglave},
[549]147  title = {The semantics of {x86-CC} multiprocessor machine code},
[1199]148  booktitle = {POPL},
[549]149  pages = {379--391},
150  year = {2009}
151}
[550]152
[568]153@inproceedings
154{ shankar:principles:1999,
[1199]155  author = {N. Shankar and S. Owre},
[568]156  title = {Principles and Pragmatics of Subtyping in {PVS}},
157  booktitle = {Recent Trends in Algebraic Development Techniques},
158  pages = {37--52},
159  year = {1999}
160}
161
162@inproceedings
163{ sozeau:subset:2006,
[1199]164  author = {M. Sozeau},
[568]165  title = {Subset coercions in {Coq}},
[1199]166  booktitle = {{TYPES}},
[568]167  pages = {237--252},
168  year = {2006}
169}
170
[814]171@inproceedings
172{ xi:guarded:2003,
[1199]173  author = {H. Xi and C. Chen and G. Chen},
[814]174  title = {Guarded recursive datatype constructors},
[1199]175  booktitle = {POPL},
[814]176  pages = {224--235},
177  year = {2003}
178}
179
[550]180@misc
[551]181{ cerco:2011,
[1199]182  title = {The {CerCo} Project},
[551]183  howpublished = {\url{http://cerco.cs.unibo.it}},
184  year = {2011},
185  key = {{CerCo}}
186}
187
188@misc
[819]189{ cerco-report-code:2011,
190  title = {{CerCo Deliverable D4.1}: executable formal semantics of machine code},
191  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf} and \url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1_Code.tar.gz}},
[579]192  year = {2011},
[819]193  key = {{CerCo-report-code}}
[579]194}
195
196@misc
[550]197{ mcu8051ide:2010,
198  title = {{MCU 8051 IDE} 1.3.11},
199  howpublished = {\url{http://mcu8051ide.sourceforge.net/}},
200  year = {2010},
201  key = {{MCU}}
202}
203
204@misc
[817]205{ moore:grand:2005,
[1199]206  author = {J S. Moore},
[817]207  title = {A Grand Challenge Proposal for Formal Methods},
208  year = {2005}
209}
210
211@misc
[555]212{ oliboni:matita:2008,
[1199]213  author = {C. A. Oliboni},
[555]214  title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}},
[1199]215  institution = {Universit\`a di Bologna},
[555]216  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
217  year = {2008}
218}
219
220@misc
[550]221{ sdcc:2010,
[819]222  title = {Small Device {C} Compiler 3.0.0},
[550]223  howpublished = {\url{http://sdcc.sourceforge.net/}},
224  year = {2010},
225  key = {{SDCC}}
226}
[551]227
[555]228@misc
229{ siemens:2011,
[557]230  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
[555]231  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
232  year = {2011},
233  key = {{Siemens}}
234}
235
[551]236@techreport
237{ amadio:certifying:2010,
[1199]238  author = {R. M. Amadio and N. Ayache and Y. R\'{e}gis-Gianas and R. Saillard},
[551]239  title = {Cerifying cost annotations in compilers},
[1199]240  institution = {Universit\'{e} Paris Diderot},
[551]241  year = {2010}
242}
Note: See TracBrowser for help on using the repository browser.