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

Last change on this file since 2714 was 2095, checked in by mulligan, 7 years ago

Added reference to CompCert? and CompCertTSO.

File size: 7.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 = {{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, 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 for Proofs and Programs},
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{ boender:correctness:2012,
98  author = {Jaap Boender and Claudio {Sacerdoti Coen}},
99  title = {On the correctness of a branch displacement algorithm},
100  booktitle = {Certified Proofs and Programs {(CPP)}},
101  year =  {2012},
102  note = {Submitted}
103}
104
105@inproceedings
106{ fox:trustworthy:2010,
107  author = {Anthony Fox and Magnus O. Myreen},
108  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
109  booktitle = {{ITP}},
110  pages = {243--258},
111  year = {2010}
112}
113
114@inproceedings
115{ sevcik:relaxed-memory:2011,
116  author = {Jaroslav \v{S}ev\v{c}\'ik and Viktor Vafeiadis and  Francesco {Zappa Nardelli} and Suresh Jagannathan and Peter Sewell},
117  title = {Relaxed-Memory Concurrency and Verified Compilation},
118  booktitle = {Principles of Programming Languages {(POPL)}},
119  year = {2011}
120}
121
122@inproceedings
123{ tuch:types:2007,
124  author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
125  title = {Types, Bytes, and Separation Logic},
126  booktitle = {Principles of Programming Languages {(POPL)}},
127  pages = {97--108},
128  year =  {2007}
129}
130
131
132@inproceedings
133{ klein:sel4:2009,
134  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},
135  title = {{seL4}: Formal verification of an operating system kernel},
136  booktitle = {{ACM} Symposium on Operating Systems Principles {(SOSP)}},
137  year = {2009}
138}
139
140@inproceedings
141{ mulligan:executable:2011,
142  author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
143  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
144  booktitle = {{FMCAD}},
145  year = {2011},
146  note = {Submitted}
147}
148
149@inproceedings
150{ sarkar:semantics:2009,
151  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},
152  title = {The semantics of {x86-CC} multiprocessor machine code},
153  booktitle = {{POPL}},
154  pages = {379--391},
155  year = {2009}
156}
157
158@inproceedings
159{ sozeau:subset:2006,
160  author = {Matthieu Sozeau},
161  title = {Subset Coercions in {Coq}},
162  booktitle = {Types for proofs and programs},
163  pages = {237--252},
164  year = {2006}
165}
166
167@inproceedings
168{ yan:wcet:2008,
169  author = {Jun Yan and Wei Zhang},
170  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
171  booktitle = {{RTAS}},
172  pages = {80--89},
173  year = {2008}
174}
175
176@misc
177{ cerco:2011,
178  title = {The {CerCo} {FET-Open} project},
179  howpublished = {\url{http://cerco.cs.unibo.it/}},
180  year = {2011},
181  key = {cerco:2011}
182}
183
184@misc
185{ cerco-report-code:2011,
186  title = {{CerCo Deliverable D2.2}: prototype cost-preserving {C} compiler},
187  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}},
188  year = {2011},
189  key = {cerco-2.2-report-code:2011}
190}
191
192@misc
193{ compcert:2011,
194  title = {The {CompCert} project},
195  howpublished = {\url{http://compcert.inria.fr/}},
196  year = {2011},
197  key = {compcert:2011}
198}
199
200@misc
201{ hyde:branch:2006,
202  title = {Branch displacement optimisation},
203  howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
204  year = {2006},
205  key = {hyde:branch:2006}
206}
207
208@misc
209{ moore:grand:2005,
210  author = {J Strother Moore},
211  title = {A Grand Challenge Proposal for Formal Methods},
212  year = {2005}
213}
214
215@misc
216{ sdcc:2011,
217  title = {Small Device {C} Compiler 3.0.0},
218  howpublished = {\url{http://sdcc.sourceforge.net/}},
219  year = {2011},
220  key = {sdcc:2010}
221}
222
223@misc
224{ sel4:2011,
225  title = {The {l4.verified} project},
226  howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
227  year = {2011}
228}
229
230@misc
231{ siemens:2011,
232  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
233  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
234  year = {2011},
235  key = {siemens:2011}
236}
237
238@techreport
239{ amadio:certifying:2010,
240  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
241  title = {Cerifying cost annotations in compilers},
242  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
243  year = {2010}
244}
245
246@techreport
247{ klein:machine:2010,
248  author = {Gerwin Klein and Tobias Nipkow},
249  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
250  institution = {National {ICT} Australia},
251  number = {0400001T.1},
252  year = {2010}
253
254}
Note: See TracBrowser for help on using the repository browser.