source: Papers/sttt/biblio.bib @ 3477

Last change on this file since 3477 was 3477, checked in by mulligan, 5 years ago

changes to intro, in progress...

File size: 12.2 KB
Line 
1@article
2{ asperti:user:2007,
3  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
4  title = {User interaction with the {Matita} proof assistant},
5  journal = {Automated Reasoning},
6  pages = {109--139},
7  volume = {39},
8  issue = {2},
9  year = {2007}
10}
11
12@article
13{ bate:wcet:2011,
14  author = {Iain Bate and Usman Khan},
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
24{ klein:machine:2006,
25  author = {Gerwin Klein and Tobias Nipkow},
26  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
27  journal = {{ACM} Transactions on Programming Languages and Systems},
28  volume = {28}, 
29  number = {4}, 
30  pages = {619--695},
31  year = {2006}
32}
33
34@article
35{ klein:sel4:2010,
36  author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood},
37  title = {{seL4}: Formal verification of an operating system kernel},
38  journal = {Communications of the {ACM}},
39  issue = {6},
40  volume = {53},
41  pages = {107--115},
42  year = {2010}
43}
44
45@article
46{ leroy:formal:2009,
47  author = {Xavier Leroy},
48  title = {Formal verification of a realistic compiler},
49  journal = {Communications of the {ACM}},
50  volume = {52},
51  number = {7},
52  pages = {107--115},
53  year = {2009}
54}
55
56@article
57{ leroy:formally:2009,
58  author = {Xavier Leroy},
59  title = {A formally verified compiler back-end},
60  journal = {Automated Reasoning},
61  volume = {43},
62  number = {4},
63  pages = {363--446},
64  year = {2009}
65}
66
67@book
68{ moore:piton:1996,
69  author = {J Strother Moore},
70  title = {Piton: A mechanically verified assembly language},
71  series = {Automated Reasoning Series},
72  volume = {3},
73  isbn = {978-0-7923-3920-5},
74  publisher = {Springer},
75  year = {1996}
76}
77
78@inproceedings
79{ atkey:coqjvm:2007,
80  author = {Robert Atkey},
81  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
82  booktitle = {Types},
83  pages = {18--32},
84  year = {2007}
85}
86
87@inproceedings
88{ blazy:formal:2006,
89  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
90  title = {Formal Verification of a {C} Compiler Front-End},
91  booktitle = {{FM}},
92  pages = {460--475},
93  year = {2006}
94}
95
96@inproceedings
97{ fox:trustworthy:2010,
98  author = {Anthony Fox and Magnus O. Myreen},
99  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
100  booktitle = {{ITP}},
101  pages = {243--258},
102  year = {2010}
103}
104
105@inproceedings
106{ sevcik:relaxed-memory:2011,
107  author = {Jaroslav \v{S}ev\v{c}\'ik and Viktor Vafeiadis and  Francesco {Zappa Nardelli} and Suresh Jagannathan and Peter Sewell},
108  title = {Relaxed-Memory Concurrency and Verified Compilation},
109  booktitle = {{POPL}},
110  year = {2011}
111}
112
113@inproceedings
114{ tuch:types:2007,
115  author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
116  title = {Types, Bytes, and Separation Logic},
117  booktitle = {{POPL}},
118  pages = {97--108},
119  year =  {2007}
120}
121
122
123@inproceedings
124{ klein:sel4:2009,
125  author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood},
126  title = {{seL4}: Formal verification of an operating system kernel},
127  booktitle = {{SOSP}},
128  year = {2009}
129}
130
131@inproceedings
132{ mulligan:executable:2011,
133  author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
134  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
135  booktitle = {{FMCAD}},
136  year = {2011},
137  note = {Submitted}
138}
139
140@inproceedings
141{ sarkar:semantics:2009,
142  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},
143  title = {The semantics of {x86-CC} multiprocessor machine code},
144  booktitle = {{POPL}},
145  pages = {379--391},
146  year = {2009}
147}
148
149@inproceedings
150{ sozeau:subset:2006,
151  author = {Matthieu Sozeau},
152  title = {Subset Coercions in {Coq}},
153  booktitle = {Types},
154  pages = {237--252},
155  year = {2006}
156}
157
158@inproceedings
159{ yan:wcet:2008,
160  author = {Jun Yan and Wei Zhang},
161  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
162  booktitle = {{RTAS}},
163  pages = {80--89},
164  year = {2008}
165}
166
167@misc
168{ boender:correctness:2012,
169  author = {Jaap Boender and Claudio {Sacerdoti Coen}},
170  title = {On the correctness of a branch displacement algorithm},
171  howpublished = {\url{http://arxiv.org/abs/1209.5920}},
172  year = {2012}
173}
174
175@misc
176{ cerco:2011,
177  title = {The {CerCo} {FET-Open} project},
178  howpublished = {\url{http://cerco.cs.unibo.it/}},
179  year = {2011},
180  key = {CerCo:2011}
181}
182
183@misc
184{ cerco-report-code:2011,
185  title = {{CerCo Deliverable D2.2}: prototype cost-preserving {C} compiler},
186  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D2_2.pdf} and \url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D2_2_Code.tar.gz}},
187  year = {2011},
188  key = {CerCo-2.2-Report-Code:2011}
189}
190
191@misc
192{ compcert:2011,
193  title = {The {CompCert} project},
194  howpublished = {\url{http://compcert.inria.fr/}},
195  year = {2011},
196  key = {CompCert:2011}
197}
198
199@misc
200{ hyde:branch:2006,
201  title = {Branch displacement optimisation},
202  howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
203  year = {2006},
204  key = {Hyde:Branch:2006}
205}
206
207@misc
208{ moore:grand:2005,
209  author = {J Strother Moore},
210  title = {A Grand Challenge Proposal for Formal Methods},
211  year = {2005}
212}
213
214@misc
215{ sdcc:2011,
216  title = {Small Device {C} Compiler 3.0.0},
217  howpublished = {\url{http://sdcc.sourceforge.net/}},
218  year = {2011},
219  key = {sdcc:2010}
220}
221
222@misc
223{ sel4:2011,
224  title = {The {l4.verified} project},
225  howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
226  year = {2011}
227}
228
229@misc
230{ siemens:2011,
231  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
232  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
233  year = {2011},
234  key = {siemens:2011}
235}
236
237@techreport
238{ amadio:certifying:2010,
239  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
240  title = {Cerifying cost annotations in compilers},
241  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
242  year = {2010}
243}
244
245@techreport
246{ klein:machine:2010,
247  author = {Gerwin Klein and Tobias Nipkow},
248  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
249  institution = {National {ICT} Australia},
250  number = {0400001T.1},
251  year = {2010}
252
253}
254
255
256@article{Szymanski1978,
257 author = {Szymanski, Thomas G.},
258 title = {Assembling code for machines with span-dependent instructions},
259 journal = {Commun. ACM},
260 issue_date = {April 1978},
261 volume = {21},
262 number = {4},
263 month = apr,
264 year = {1978},
265 issn = {0001-0782},
266 pages = {300--308},
267 numpages = {9},
268 url = {http://doi.acm.org/10.1145/359460.359474},
269 doi = {10.1145/359460.359474},
270 acmid = {359474},
271 publisher = {ACM},
272 address = {New York, NY, USA},
273 keywords = {NP-complete, assemblers, code generation, compilers, computational complexity, span-dependent instructions, variable-length addressing},
274} 
275
276@article{Robertson1979,
277 author = {Robertson, Edward L.},
278 title = {Code Generation and Storage Allocation for Machines with Span-Dependent Instructions},
279 journal = {ACM Trans. Program. Lang. Syst.},
280 issue_date = {July 1979},
281 volume = {1},
282 number = {1},
283 month = jan,
284 year = {1979},
285 issn = {0164-0925},
286 pages = {71--83},
287 numpages = {13},
288 url = {http://doi.acm.org/10.1145/357062.357067},
289 doi = {10.1145/357062.357067},
290 acmid = {357067},
291 publisher = {ACM},
292 address = {New York, NY, USA},
293} 
294
295@article{Dickson2008,
296  author    = {Neil G. Dickson},
297  title     = {A Simple, Linear-Time Algorithm for x86 Jump Encoding},
298  journal   = {CoRR},
299  volume    = {abs/0812.4973},
300  year      = {2008},
301  ee        = {http://arxiv.org/abs/0812.4973},
302  bibsource = {DBLP, http://dblp.uni-trier.de}
303}
304
305@inproceedings{Sozeau2006,
306  author = {Matthieu Sozeau},
307  title = {Subset Coercions in {Coq}},
308  booktitle = {{TYPES}},
309  pages = {237--252},
310  year = {2006}
311}
312
313@misc{SDCC2011,
314  title = {Small Device {C} Compiler 3.1.0},
315  howpublished = {\url{http://sdcc.sourceforge.net/}},
316  year = {2011},
317        key = {SDCC2011}
318}
319
320@misc{IntelDev,
321        author = {Intel},
322        title = {{Intel 64 and IA-32 Architectures Developer's Manual}},
323        howpublished={\url{http://www.intel.com/content/www/us/en/processors/architectures-software-developer-manuals.html}},
324        volume=2,
325  key = {IntelDev}
326}
327
328@article {Leroy2009,
329   author = {Leroy, Xavier},
330   affiliation = {INRIA Paris-Rocquencourt B.P. 105 78153 Le Chesnay France},
331   title = {A Formally Verified Compiler Back-end},
332   journal = {Journal of Automated Reasoning},
333   publisher = {Springer Netherlands},
334   issn = {0168-7433},
335   keyword = {Computer Science},
336   pages = {363-446},
337   volume = {43},
338   issue = {4},
339   url = {http://dx.doi.org/10.1007/s10817-009-9155-4},
340   note = {10.1007/s10817-009-9155-4},
341   year = {2009}
342}
343
344@book {Moore1996, 
345  author = {J Strother Moore},
346  title = {Piton: A mechanically verified assembly language},
347  series = {Automated Reasoning Series},
348  volume = {3},
349  isbn = {978-0-7923-3920-5},
350  publisher = {Springer},
351  year = {1996}
352}
353
354@misc {Hyde2006,
355  title = {Branch displacement optimisation},
356        author = {Randall Hyde},
357  howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
358  year = {2006},
359}
360
361@misc{DC2012,
362        title={{On the correctness of an optimising assembler for the Intel MCS-51 microprocessor}},
363        author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
364        year = {2012},
365        booktitle = {Certified Proofs and Programs {(CPP)}},
366        note = {Submitted}
367}
368
369@article{Asperti2007,
370  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
371  title = {User interaction with the {Matita} proof assistant},
372  journal = {Automated Reasoning},
373  pages = {109--139},
374  volume = {39},
375  issue = {2},
376  year = {2007}
377}
378
379@article{TSO2011,
380 author = {\v{S}ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
381 title = {Relaxed-memory concurrency and verified compilation},
382 journal = {SIGPLAN Not.},
383 issue_date = {January 2011},
384 volume = {46},
385 number = {1},
386 month = jan,
387 year = {2011},
388 issn = {0362-1340},
389 pages = {43--54},
390 numpages = {12},
391 url = {http://doi.acm.org/10.1145/1925844.1926393},
392 doi = {10.1145/1925844.1926393},
393 acmid = {1926393},
394 publisher = {ACM},
395 address = {New York, NY, USA},
396 keywords = {relaxed memory models, semantics, verifying compilation},
397} 
398
399@inproceedings{Sevcik:2011:RCV:1926385.1926393,
400 author = {\v{S}ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
401 title = {Relaxed-memory concurrency and verified compilation},
402 booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
403 series = {POPL '11},
404 year = {2011},
405 isbn = {978-1-4503-0490-0},
406 location = {Austin, Texas, USA},
407 pages = {43--54},
408 numpages = {12},
409 url = {http://doi.acm.org/10.1145/1926385.1926393},
410 doi = {10.1145/1926385.1926393},
411 acmid = {1926393},
412 publisher = {ACM},
413 address = {New York, NY, USA},
414 keywords = {relaxed memory models, semantics, verifying compilation},
415} 
416
417@incollection{lastyear,
418year={2012},
419isbn={978-3-642-35307-9},
420booktitle={Certified Programs and Proofs},
421volume={7679},
422series={Lecture Notes in Computer Science},
423editor={Hawblitzel, Chris and Miller, Dale},
424doi={10.1007/978-3-642-35308-6_7},
425title={On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor},
426url={http://dx.doi.org/10.1007/978-3-642-35308-6_7},
427publisher={Springer Berlin Heidelberg},
428keywords={Verified software; CerCo (Certified Complexity); MCS-51 microcontroller; Matita proof assistant},
429author={Mulligan, Dominic P. and Sacerdoti Coen, Claudio},
430pages={43-59}
431}
432
433@misc
434{ compcert:2011,
435  title = {The {CompCert} project},
436  howpublished = {\url{http://compcert.inria.fr/}},
437  year = {2011},
438  key = {compcert:2011}
439}
Note: See TracBrowser for help on using the repository browser.