source: Papers/jar-cerco-2017/cerco.bib @ 3611

Last change on this file since 3611 was 3605, checked in by mulligan, 3 years ago

bib file

File size: 9.6 KB
Line 
1@TechReport{survey,
2 author = {W. W\"ogerer},
3 title = {A Survey of Static Program Analysis Techniques},
4 institution = {Technische Universit\"at Wien},
5 year = {2005}
6}
7
8
9@article{cerco,
10  INIauthor    = {R. Amadio and A. Asperti and N. Ayache and
11                  B. Campbell and D. P. Mulligan and R. Pollack and
12                  Y. R{\'e}gis-Gianas and C. Sacerdoti Coen and I.
13                  Stark},
14  author    = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
15                  Brian Campbell and Dominic P. Mulligan and Randy Pollack and
16                  Yann R{\'e}gis-Gianas and Claudio Sacerdoti Coen and Ian
17                  Stark},
18  title     = {Certified Complexity},
19  journal   = {Procedia Computer Science},
20  volume    = 7,
21  year      = 2011,
22  pages     = {175--177},
23  doi       = {10.1016/j.procs.2011.09.054},
24  note      = {Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11)}
25}
26
27@incollection{labelling,
28year={2012},
29isbn={978-3-642-32468-0},
30booktitle={Formal Methods for Industrial Critical Systems},
31volume={7437},
32series={LNCS},
33doi={10.1007/978-3-642-32469-7_3},
34title={Certifying and Reasoning on Cost Annotations in {C} Programs},
35url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
36author={Ayache, Nicolas and Amadio, Roberto and R\'egis-Gianas, Yann},
37pages={32--46},
38publisher={Springer Berlin Heidelberg}
39}
40
41@incollection{labelling2,
42year={2012},
43booktitle={Foundational and Practical Aspects of Resource Analysis},
44volume={7177},
45series={LNCS},
46doi={10.1007/978-3-642-32495-6_5},
47title={Certifying and Reasoning on Cost Annotations of Functional Programs},
48author={Amadio, Roberto and R\'egis-Gianas, Yann},
49pages={72--89},
50note={Extended version to appear in Higher Order and Symbolic Computation},
51publisher={Springer Berlin Heidelberg}
52}
53
54@article{compcert,
55  author = {Xavier Leroy},
56  title = {Formal verification of a realistic compiler},
57  journal = {Communications of the ACM},
58  year = 2009,
59  volume = 52,
60  number = 7,
61  pages = {107--115},
62  urlthatwewillskip = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
63  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
64  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
65  pubkind = {journal-int-mono},
66  abstract = {This paper reports on the development and formal verification (proof
67of semantic preservation) of CompCert, a compiler from Clight (a
68large subset of the C programming language) to PowerPC assembly code,
69using the Coq proof assistant both for programming the compiler and
70for proving its correctness.  Such a verified compiler is useful in
71the context of critical software and its formal verification: the
72verification of the compiler guarantees that the safety properties
73proved on the source code hold for the executable compiled code as
74well.}
75}
76
77@Manual{framac,
78title = {Frama-{C} user manual},
79author = {L. Correnson and P. Cuoq and F. Kirchner and V. Prevosto and A. Puccetti and J. Signoles and
80B. Yakobowski},
81organization = {CEA-LIST, Software Safety Laboratory, Saclay, F-91191},
82note = {\url{http://frama-c.com/}}
83}
84
85@inproceedings{paolo,
86 author = {Paolo Tranquilli},
87 title = {Indexed Labels for Loop Iteration Dependent Costs},
88 booktitle = {QAPL},
89 series = {EPTCS},
90 volume = {117},
91 doi = {10.4204/EPTCS.117.2},
92 year = {2013},
93 pages = {19--23}
94}
95
96@INPROCEEDINGS{separation,
97    author = {John C. Reynolds},
98    title = {Intuitionistic Reasoning about Shared Mutable Data Structure},
99    booktitle = {Millennial Perspectives in Computer Science},
100    year = {2000},
101    pages = {303--321},
102    publisher = {Palgrave}
103}
104
105@inproceedings{lustre,
106  author    = {Paul Caspi and
107               Daniel Pilaud and
108               Nicolas Halbwachs and
109               John Plaice},
110  title     = {Lustre: A Declarative Language for Programming Synchronous
111               Systems},
112  booktitle = {POPL},
113  year      = {1987},
114  pages     = {178-188},
115  ee        = {http://doi.acm.org/10.1145/41625.41641},
116  crossref  = {DBLP:conf/popl/1987},
117  bibsource = {DBLP, http://dblp.uni-trier.de}
118}
119@proceedings{DBLP:conf/popl/1987,
120  title     = {Conference Record of the Fourteenth Annual ACM Symposium
121               on Principles of Programming Languages, Munich, Germany,
122               January 21-23, 1987},
123  booktitle = {POPL},
124  publisher = {ACM Press},
125  year      = {1987},
126  isbn      = {0-89791-215-2},
127  ee        = {http://dl.acm.org/citation.cfm?id=41625},
128  bibsource = {DBLP, http://dblp.uni-trier.de}
129}
130 
131@inproceedings{correctness,
132  author    = {Mulligan, Dominic P.  and
133               Sacerdoti Coen, Claudio},
134  title     = {On the Correctness of an Optimising Assembler for the {Intel
135               MCS-51} Microprocessor},
136  booktitle = {CPP},
137  year      = {2012},
138  pages     = {43--59},
139  doi       = {10.1007/978-3-642-35308-6_7}
140}
141@proceedings{DBLP:conf/cpp/2012,
142  editor    = {Chris Hawblitzel and
143               Dale Miller},
144  title     = {Certified Programs and Proofs - Second International Conference,
145               CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
146  booktitle = {CPP},
147  publisher = {Springer},
148  series    = {LNCS},
149  volume    = {7679},
150  year      = {2012},
151  isbn      = {978-3-642-35307-9},
152  ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6},
153  bibsource = {DBLP, http://dblp.uni-trier.de}
154}
155
156@article{proartis,
157    title = {PROARTIS: Probabilistically Analysable Real-Time Systems},
158    journal = {Transactions on Embedded Computing Systems},
159    year = {2012},
160    publisher = {ACM},
161    author = {Francisco Cazorla and Eduardo Qui{\~n}ones and Tullio Vardanega and Liliana Cucu and Benoit Triquet and Guillem Bernat and Emery Berger and Jaume Abella and Franck Wartel and Michael Houston and Luca Santinelli and Leonidas Kosmidis and Code Lo and Dorin Maxim}
162}
163
164@inproceedings{embounded,
165  author    = {Kevin Hammond and
166               Roy Dyckhoff and
167               Christian Ferdinand and
168               Reinhold Heckmann and
169               Martin Hofmann and
170               Steffen Jost and
171               Hans-Wolfgang Loidl and
172               Greg Michaelson and
173               Robert F. Pointon and
174               Norman Scaife and
175               Jocelyn S{\'e}rot and
176               Andy Wallace},
177  title     = {{The {EmBounded} Project (Project Start Paper)}},
178  booktitle = {TFP},
179  year      = {2005},
180  pages     = {195--210},
181  crossref  = {TFP2005},
182}
183
184@proceedings{TFP2005,
185  title     = {Revised Selected Papers from the Sixth Symposium on Trends
186               in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
187               September 2005},
188  booktitle = {Trends in Functional Programming},
189  series    = {Trends in Functional Programming},
190  volume    = {6},
191  year      = {2007},
192  isbn      = {978-1-84150-176-5},
193}
194
195@inproceedings{matita,
196  author    = {Andrea Asperti and
197               Wilmer Ricciotti and
198               Claudio Sacerdoti Coen and
199               Enrico Tassi},
200  title     = {The {Matita} Interactive Theorem Prover},
201  booktitle = {CADE},
202  year      = {2011},
203  pages     = {64-69},
204  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6_7},
205  crossref  = {DBLP:conf/cade/2011},
206  bibsource = {DBLP, http://dblp.uni-trier.de}
207}
208@proceedings{DBLP:conf/cade/2011,
209  title     = {Automated Deduction - CADE-23 - 23rd International Conference
210               on Automated Deduction, Wroclaw, Poland, July 31 - August
211               5, 2011. Proceedings},
212  booktitle = {CADE},
213  publisher = {Springer},
214  series    = {LNCS},
215  volume    = {6803},
216  year      = {2011},
217  isbn      = {978-3-642-22437-9},
218  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6},
219  bibsource = {DBLP, http://dblp.uni-trier.de}
220}
221
222@article{typeffects,
223  author    = {Jean-Pierre Talpin and
224               Pierre Jouvelot},
225  title     = {The Type and Effect Discipline},
226  journal   = {Inf. Comput.},
227  volume    = {111},
228  number    = {2},
229  year      = {1994},
230  pages     = {245-296},
231  ee        = {http://dx.doi.org/10.1006/inco.1994.1046},
232  bibsource = {DBLP, http://dblp.uni-trier.de}
233}
234
235@article{stateart,
236  author    = {Reinhard Wilhelm and
237               Jakob Engblom and
238               Andreas Ermedahl and
239               Niklas Holsti and
240               Stephan Thesing and
241               David B. Whalley and
242               Guillem Bernat and
243               Christian Ferdinand and
244               Reinhold Heckmann and
245               Tulika Mitra and
246               Frank Mueller and
247               Isabelle Puaut and
248               Peter P. Puschner and
249               Jan Staschulat and
250               Per Stenstr{\"o}m},
251  title     = {The worst-case execution-time problem---overview of methods
252               and survey of tools},
253  journal   = {ACM Trans. Embedded Comput. Syst.},
254  volume    = {7},
255  number    = {3},
256  year      = {2008},
257  ee        = {http://doi.acm.org/10.1145/1347375.1347389},
258  bibsource = {DBLP, http://dblp.uni-trier.de}
259}
260
261@inproceedings{bobot,
262  year={2012},
263  booktitle={Formal Methods and Software Engineering},
264  volume={7635},
265  series={Lecture Notes in Computer Science},
266  doi={10.1007/978-3-642-34281-3_14},
267  title={Separation Predicates: A Taste of Separation Logic in First-Order Logic},
268  url={http://dx.doi.org/10.1007/978-3-642-34281-3_14},
269  author={Bobot, François and Filliâtre, Jean-Christophe},
270  pages={167-181}
271}
272
273@misc
274{ absint,
275  url = {http://www.absint.com/ait/},
276  author = {{AbsInt}},
277  title = {{aiT WCET} analysis tools}
278}
279
280@misc
281{ cerco-website,
282  url = {http://cerco.cs.unibo.it},
283  title = {The {Certified Complexity} ({CerCo}) project web site},
284  key = {cerco}
285}
286
287@misc
288{ jessie,
289  url = {http://krakatoa.lri.fr/},
290  title = {Jessie {Frama-C} plugin},
291  key = {jessie}
292}
Note: See TracBrowser for help on using the repository browser.