source: src/ASM/CPP2012-asm/cpp-2012-asm.bib @ 2067

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

Added Randall Holmes' Usenet post on branch displacement optimisation to the bibliography.

File size: 6.0 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 = {{TOPLAS}},
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, Harvey Tuch and Simon Winwood},
37  title = {{seL4}: Formal verification of an operating system kernel},
38  journal = {{CACM}},
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 = {{CACM}},
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{ klein:sel4:2009,
107  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, Harvey Tuch and Simon Winwood},
108  title = {{seL4}: Formal verification of an operating system kernel},
109  booktitle = {{SOSP}},
110  year = {2009}
111}
112
113@inproceedings
114{ mulligan:executable:2011,
115  author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
116  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
117  booktitle = {{FMCAD}},
118  year = {2011},
119  note = {Submitted}
120}
121
122@inproceedings
123{ sarkar:semantics:2009,
124  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},
125  title = {The semantics of {x86-CC} multiprocessor machine code},
126  booktitle = {{POPL}},
127  pages = {379--391},
128  year = {2009}
129}
130
131@inproceedings
132{ sozeau:subset:2006,
133  author = {Matthieu Sozeau},
134  title = {Subset Coercions in {Coq}},
135  booktitle = {{TYPES}},
136  pages = {237--252},
137  year = {2006}
138}
139
140@inproceedings
141{ yan:wcet:2008,
142  author = {Jun Yan and Wei Zhang},
143  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
144  booktitle = {{RTAS}},
145  pages = {80--89},
146  year = {2008}
147}
148
149@misc
150{ cerco:2011,
151  title = {The {CerCo} {FET-Open} project},
152  howpublished = {\url{http://cerco.cs.unibo.it/}},
153  year = {2011},
154  key = {cerco:2011}
155}
156
157@misc
158{ cerco-report-code:2011,
159  title = {{CerCo Deliverable D2.2}: prototype cost-preserving {C} compiler},
160  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}},
161  year = {2011},
162  key = {cerco-2.2-report-code:2011}
163}
164
165@misc
166{ compcert:2011,
167  title = {The {CompCert} project},
168  howpublished = {\url{http://compcert.inria.fr/}},
169  year = {2011},
170  key = {compcert:2011}
171}
172
173@misc
174{ holmes:branch:2006,
175  title = {Branch displacement optimisation},
176  howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
177  year = {2006},
178  key = {holmes:branch:2006}
179}
180
181@misc
182{ moore:grand:2005,
183  author = {J Strother Moore},
184  title = {A Grand Challenge Proposal for Formal Methods},
185  year = {2005}
186}
187
188@misc
189{ sdcc:2011,
190  title = {Small Device {C} Compiler 3.0.0},
191  howpublished = {\url{http://sdcc.sourceforge.net/}},
192  year = {2011},
193  key = {sdcc:2010}
194}
195
196@misc
197{ sel4:2011,
198  title = {The {l4.verified} project},
199  howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
200  year = {2011}
201}
202
203@misc
204{ siemens:2011,
205  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
206  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
207  year = {2011},
208  key = {siemens:2011}
209}
210
211@techreport
212{ amadio:certifying:2010,
213  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
214  title = {Cerifying cost annotations in compilers},
215  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
216  year = {2010}
217}
218
219@techreport
220{ klein:machine:2010,
221  author = {Gerwin Klein and Tobias Nipkow},
222  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
223  institution = {National {ICT} Australia},
224  number = {0400001T.1},
225  year = {2010}
226
227}
Note: See TracBrowser for help on using the repository browser.