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

Last change on this file since 1020 was 1020, checked in by sacerdot, 8 years ago

More on Matita.

File size: 6.6 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 = {Journal of 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 = {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 {Association of Computing Machinery}},
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 = {Journal of 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 = {Conference of the {TYPES} Project},
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 = {International Symposium on Formal Methods},
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 = {$\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
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 = {Proceedings of the $22^\mathrm{nd}$ {ACM} Symposium on Operating Systems Principles},
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 = {Formal Methods in Computer Aided Design},
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 = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
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 for Proofs and Programs},
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 = {$\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
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}
220
221@inproceedings{russell,
222  author    = {Matthieu Sozeau},
223  title     = {Subset Coercions in {C}oq},
224  booktitle = {Types for Proofs and Programs},
225  series    = {LNCS},
226  year      = {2006},
227  pages     = {237-252},
228  VOLUME = {4502/2007},
229  PUBLISHER = {Springer-Verlag},
230  doi = {10.1007/978-3-540-74464-1\_16},
231}
Note: See TracBrowser for help on using the repository browser.