source: Papers/cpp-2011/cpp-2011.bib @ 3346

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

final version? under 16 pages

File size: 5.8 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{ moore:grand:2005,
175  author = {J Strother Moore},
176  title = {A Grand Challenge Proposal for Formal Methods},
177  year = {2005}
178}
179
180@misc
181{ sdcc:2011,
182  title = {Small Device {C} Compiler 3.0.0},
183  howpublished = {\url{http://sdcc.sourceforge.net/}},
184  year = {2011},
185  key = {sdcc:2010}
186}
187
188@misc
189{ sel4:2011,
190  title = {The {l4.verified} project},
191  howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
192  year = {2011}
193}
194
195@misc
196{ siemens:2011,
197  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
198  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
199  year = {2011},
200  key = {siemens:2011}
201}
202
203@techreport
204{ amadio:certifying:2010,
205  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
206  title = {Cerifying cost annotations in compilers},
207  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
208  year = {2010}
209}
210
211@techreport
212{ klein:machine:2010,
213  author = {Gerwin Klein and Tobias Nipkow},
214  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
215  institution = {National {ICT} Australia},
216  number = {0400001T.1},
217  year = {2010}
218
219}
Note: See TracBrowser for help on using the repository browser.