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

Last change on this file since 960 was 960, checked in by mulligan, 9 years ago

more work on paper

File size: 4.2 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:sel4:2010,
25  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},
26  title = {{seL4}: Formal verification of an operating system kernel},
27  journal = {Communications of the {ACM}},
28  issue = {6},
29  volume = {53},
30  pages = {107--115},
31  year = {2010}
32}
33
34@article
35{ leroy:formal:2009,
36  author = {Xavier Leroy},
37  title = {Formal verification of a realistic compiler},
38  journal = {Communications of the {Association of Computing Machinery}},
39  volume = {52},
40  number = {7},
41  pages = {107--115},
42  year = {2009}
43}
44
45@article
46{ leroy:formally:2009,
47  author = {Xavier Leroy},
48  title = {A formally verified compiler back-end},
49  journal = {Journal of Automated Reasoning},
50  volume = {43},
51  number = {4},
52  pages = {363--446},
53  year = {2009}
54}
55
56@inproceedings
57{ blazy:formal:2006,
58  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
59  title = {Formal Verification of a {C} Compiler Front-End},
60  booktitle = {International Symposium on Formal Methods},
61  pages = {460--475},
62  year = {2006}
63}
64
65@inproceedings
66{ klein:sel4:2009,
67  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},
68  title = {{seL4}: Formal verification of an operating system kernel},
69  booktitle = {Proceedings of the $22^\mathrm{nd}$ {ACM} Symposium on Operating Systems Principles},
70  year = {2009}
71}
72
73@inproceedings
74{ mulligan:executable:2011,
75  author = {Dominic P. Mulligan and Claudio Sacerdoti Coen},
76  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
77  booktitle = {Formal Methods in Computer Aided Design},
78  year = {2011},
79  note = {Submitted}
80}
81
82@inproceedings
83{ yan:wcet:2008,
84  author = {Jun Yan and Wei Zhang},
85  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
86  booktitle = {$\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
87  pages = {80--89},
88  year = {2008}
89}
90
91@misc
92{ cerco:2011,
93  title = {The {CerCo} {FET-Open} project},
94  howpublished = {\url{http://cerco.cs.unibo.it/}},
95  year = {2011},
96  key = {cerco:2011}
97}
98
99@misc
100{ cerco-report-code:2011,
101  title = {{CerCo Deliverable D2.2}: prototype cost-preserving {C} compiler},
102  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}},
103  year = {2011},
104  key = {cerco-2.2-report-code:2011}
105}
106
107@misc
108{ compcert:2011,
109  title = {The {CompCert} project},
110  howpublished = {\url{http://compcert.inria.fr/}},
111  year = {2011},
112  key = {compcert:2011}
113}
114
115@misc
116{ sdcc:2011,
117  title = {Small Device {C} Compiler 3.0.0},
118  howpublished = {\url{http://sdcc.sourceforge.net/}},
119  year = {2011},
120  key = {sdcc:2010}
121}
122
123@misc
124{ sel4:2011,
125  title = {The {l4.verified} project},
126  howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
127  year = {2011}
128}
129
130@misc
131{ siemens:2011,
132  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
133  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
134  year = {2011},
135  key = {siemens:2011}
136}
137
138@techreport
139{ amadio:certifying:2010,
140  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
141  title = {Cerifying cost annotations in compilers},
142  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
143  year = {2010}
144}
Note: See TracBrowser for help on using the repository browser.