source: src/ASM/CPP2011/cpp-2011.bib @ 2358

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

final version? under 16 pages

File size: 5.8 KB
RevLine 
[927]1@article
[953]2{ asperti:user:2007,
[970]3  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
[953]4  title = {User interaction with the {Matita} proof assistant},
[1026]5  journal = {Automated Reasoning},
[953]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
[981]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},
[1026]27  journal = {{TOPLAS}},
[981]28  volume = {28}, 
29  number = {4}, 
30  pages = {619--695},
31  year = {2006}
32}
33
34@article
[927]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},
[1026]38  journal = {{CACM}},
[927]39  issue = {6},
40  volume = {53},
41  pages = {107--115},
42  year = {2010}
43}
44
[953]45@article
46{ leroy:formal:2009,
47  author = {Xavier Leroy},
48  title = {Formal verification of a realistic compiler},
[1026]49  journal = {{CACM}},
[953]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},
[1026]60  journal = {Automated Reasoning},
[953]61  volume = {43},
62  number = {4},
63  pages = {363--446},
64  year = {2009}
65}
66
[981]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
[953]78@inproceedings
[981]79{ atkey:coqjvm:2007,
80  author = {Robert Atkey},
81  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
[1026]82  booktitle = {{TYPES}},
[981]83  pages = {18--32},
84  year = {2007}
85}
86
87@inproceedings
[953]88{ blazy:formal:2006,
89  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
90  title = {Formal Verification of a {C} Compiler Front-End},
[1026]91  booktitle = {{FM}},
[953]92  pages = {460--475},
93  year = {2006}
94}
95
96@inproceedings
[981]97{ fox:trustworthy:2010,
98  author = {Anthony Fox and Magnus O. Myreen},
99  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
[1026]100  booktitle = {{ITP}},
[981]101  pages = {243--258},
102  year = {2010}
103}
104
105@inproceedings
[927]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},
[1026]109  booktitle = {{SOSP}},
[927]110  year = {2009}
111}
112
[953]113@inproceedings
[960]114{ mulligan:executable:2011,
[970]115  author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
[960]116  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
[1026]117  booktitle = {{FMCAD}},
[960]118  year = {2011},
119  note = {Submitted}
120}
121
122@inproceedings
[981]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},
[1026]126  booktitle = {{POPL}},
[981]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}},
[1026]135  booktitle = {{TYPES}},
[981]136  pages = {237--252},
137  year = {2006}
138}
139
140@inproceedings
[953]141{ yan:wcet:2008,
142  author = {Jun Yan and Wei Zhang},
143  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
[1026]144  booktitle = {{RTAS}},
[953]145  pages = {80--89},
146  year = {2008}
147}
148
[927]149@misc
150{ cerco:2011,
[953]151  title = {The {CerCo} {FET-Open} project},
152  howpublished = {\url{http://cerco.cs.unibo.it/}},
153  year = {2011},
154  key = {cerco:2011}
[927]155}
156
157@misc
[953]158{ cerco-report-code:2011,
[960]159  title = {{CerCo Deliverable D2.2}: prototype cost-preserving {C} compiler},
[953]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
[927]166{ compcert:2011,
167  title = {The {CompCert} project},
[953]168  howpublished = {\url{http://compcert.inria.fr/}},
169  year = {2011},
170  key = {compcert:2011}
[927]171}
172
173@misc
[981]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
[953]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
[927]189{ sel4:2011,
190  title = {The {l4.verified} project},
[953]191  howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
[927]192  year = {2011}
193}
[953]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}
[981]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.