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

Last change on this file since 3637 was 3632, checked in by mulligan, 3 years ago

Small tweaks before work on another paper

File size: 12.8 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@inproceedings{DBLP:conf/pldi/Carbonneaux0RS14,
9  author    = {Quentin Carbonneaux and
10               Jan Hoffmann and
11               Tahina Ramananandro and
12               Zhong Shao},
13  title     = {End-to-end verification of stack-space bounds for {C} programs},
14  booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
15               {PLDI} '14, Edinburgh, United Kingdom - June 09 - 11, 2014},
16  pages     = {270--281},
17  year      = {2014},
18  crossref  = {DBLP:conf/pldi/2014},
19  url       = {http://doi.acm.org/10.1145/2594291.2594301},
20  doi       = {10.1145/2594291.2594301},
21  timestamp = {Tue, 20 Dec 2016 10:12:01 +0100},
22  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/pldi/Carbonneaux0RS14},
23  bibsource = {dblp computer science bibliography, http://dblp.org}
24}
25
26
27@article{cerco,
28  INIauthor    = {R. Amadio and A. Asperti and N. Ayache and
29                  B. Campbell and D. P. Mulligan and R. Pollack and
30                  Y. R{\'e}gis-Gianas and C. Sacerdoti Coen and I.
31                  Stark},
32  author    = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
33                  Brian Campbell and Dominic P. Mulligan and Randy Pollack and
34                  Yann R{\'e}gis-Gianas and Claudio Sacerdoti Coen and Ian
35                  Stark},
36  title     = {Certified Complexity},
37  journal   = {Procedia Computer Science},
38  volume    = 7,
39  year      = 2011,
40  pages     = {175--177},
41  doi       = {10.1016/j.procs.2011.09.054},
42  note      = {Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11)}
43}
44
45@incollection{labelling,
46year={2012},
47isbn={978-3-642-32468-0},
48booktitle={Formal Methods for Industrial Critical Systems},
49volume={7437},
50series={LNCS},
51doi={10.1007/978-3-642-32469-7_3},
52title={Certifying and Reasoning on Cost Annotations in {C} Programs},
53url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
54author={Ayache, Nicolas and Amadio, Roberto and R\'egis-Gianas, Yann},
55pages={32--46},
56publisher={Springer Berlin Heidelberg}
57}
58
59@incollection{labelling2,
60year={2012},
61booktitle={Foundational and Practical Aspects of Resource Analysis},
62volume={7177},
63series={LNCS},
64doi={10.1007/978-3-642-32495-6_5},
65title={Certifying and Reasoning on Cost Annotations of Functional Programs},
66author={Amadio, Roberto and R\'egis-Gianas, Yann},
67pages={72--89},
68note={Extended version to appear in Higher Order and Symbolic Computation},
69publisher={Springer Berlin Heidelberg}
70}
71
72@article{compcert,
73  author = {Xavier Leroy},
74  title = {Formal verification of a realistic compiler},
75  journal = {Communications of the ACM},
76  year = 2009,
77  volume = 52,
78  number = 7,
79  pages = {107--115},
80  urlthatwewillskip = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
81  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
82  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
83  pubkind = {journal-int-mono},
84  abstract = {This paper reports on the development and formal verification (proof
85of semantic preservation) of CompCert, a compiler from Clight (a
86large subset of the C programming language) to PowerPC assembly code,
87using the Coq proof assistant both for programming the compiler and
88for proving its correctness.  Such a verified compiler is useful in
89the context of critical software and its formal verification: the
90verification of the compiler guarantees that the safety properties
91proved on the source code hold for the executable compiled code as
92well.}
93}
94
95@Manual{framac,
96title = {Frama-{C} user manual},
97author = {L. Correnson and P. Cuoq and F. Kirchner and V. Prevosto and A. Puccetti and J. Signoles and
98B. Yakobowski},
99organization = {CEA-LIST, Software Safety Laboratory, Saclay, F-91191},
100note = {\url{http://frama-c.com/}}
101}
102
103@inproceedings{paolo,
104 author = {Paolo Tranquilli},
105 title = {Indexed Labels for Loop Iteration Dependent Costs},
106 booktitle = {QAPL},
107 series = {EPTCS},
108 volume = {117},
109 doi = {10.4204/EPTCS.117.2},
110 year = {2013},
111 pages = {19--23}
112}
113
114@INPROCEEDINGS{separation,
115    author = {John C. Reynolds},
116    title = {Intuitionistic Reasoning about Shared Mutable Data Structure},
117    booktitle = {Millennial Perspectives in Computer Science},
118    year = {2000},
119    pages = {303--321},
120    publisher = {Palgrave}
121}
122
123@inproceedings{lustre,
124  author    = {Paul Caspi and
125               Daniel Pilaud and
126               Nicolas Halbwachs and
127               John Plaice},
128  title     = {Lustre: A Declarative Language for Programming Synchronous
129               Systems},
130  booktitle = {POPL},
131  year      = {1987},
132  pages     = {178-188},
133  ee        = {http://doi.acm.org/10.1145/41625.41641},
134  crossref  = {DBLP:conf/popl/1987},
135  bibsource = {DBLP, http://dblp.uni-trier.de}
136}
137@proceedings{DBLP:conf/popl/1987,
138  title     = {Conference Record of the Fourteenth Annual ACM Symposium
139               on Principles of Programming Languages, Munich, Germany,
140               January 21-23, 1987},
141  booktitle = {POPL},
142  publisher = {ACM Press},
143  year      = {1987},
144  isbn      = {0-89791-215-2},
145  ee        = {http://dl.acm.org/citation.cfm?id=41625},
146  bibsource = {DBLP, http://dblp.uni-trier.de}
147}
148 
149@inproceedings{correctness,
150  author    = {Mulligan, Dominic P.  and
151               Sacerdoti Coen, Claudio},
152  title     = {On the Correctness of an Optimising Assembler for the {Intel
153               MCS-51} Microprocessor},
154  booktitle = {CPP},
155  year      = {2012},
156  pages     = {43--59},
157  doi       = {10.1007/978-3-642-35308-6_7}
158}
159@proceedings{DBLP:conf/cpp/2012,
160  editor    = {Chris Hawblitzel and
161               Dale Miller},
162  title     = {Certified Programs and Proofs - Second International Conference,
163               CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
164  booktitle = {CPP},
165  publisher = {Springer},
166  series    = {LNCS},
167  volume    = {7679},
168  year      = {2012},
169  isbn      = {978-3-642-35307-9},
170  ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6},
171  bibsource = {DBLP, http://dblp.uni-trier.de}
172}
173
174@article{proartis,
175    title = {PROARTIS: Probabilistically Analysable Real-Time Systems},
176    journal = {Transactions on Embedded Computing Systems},
177    year = {2012},
178    publisher = {ACM},
179    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}
180}
181
182@inproceedings{embounded,
183  author    = {Kevin Hammond and
184               Roy Dyckhoff and
185               Christian Ferdinand and
186               Reinhold Heckmann and
187               Martin Hofmann and
188               Steffen Jost and
189               Hans-Wolfgang Loidl and
190               Greg Michaelson and
191               Robert F. Pointon and
192               Norman Scaife and
193               Jocelyn S{\'e}rot and
194               Andy Wallace},
195  title     = {{The {EmBounded} Project (Project Start Paper)}},
196  booktitle = {TFP},
197  year      = {2005},
198  pages     = {195--210},
199  crossref  = {TFP2005},
200}
201
202@proceedings{TFP2005,
203  title     = {Revised Selected Papers from the Sixth Symposium on Trends
204               in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
205               September 2005},
206  booktitle = {Trends in Functional Programming},
207  series    = {Trends in Functional Programming},
208  volume    = {6},
209  year      = {2007},
210  isbn      = {978-1-84150-176-5},
211}
212
213@inproceedings{matita,
214  author    = {Andrea Asperti and
215               Wilmer Ricciotti and
216               Claudio Sacerdoti Coen and
217               Enrico Tassi},
218  title     = {The {Matita} Interactive Theorem Prover},
219  booktitle = {CADE},
220  year      = {2011},
221  pages     = {64-69},
222  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6_7},
223  crossref  = {DBLP:conf/cade/2011},
224  bibsource = {DBLP, http://dblp.uni-trier.de}
225}
226@proceedings{DBLP:conf/cade/2011,
227  title     = {Automated Deduction - CADE-23 - 23rd International Conference
228               on Automated Deduction, Wroclaw, Poland, July 31 - August
229               5, 2011. Proceedings},
230  booktitle = {CADE},
231  publisher = {Springer},
232  series    = {LNCS},
233  volume    = {6803},
234  year      = {2011},
235  isbn      = {978-3-642-22437-9},
236  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6},
237  bibsource = {DBLP, http://dblp.uni-trier.de}
238}
239
240@article{typeffects,
241  author    = {Jean-Pierre Talpin and
242               Pierre Jouvelot},
243  title     = {The Type and Effect Discipline},
244  journal   = {Inf. Comput.},
245  volume    = {111},
246  number    = {2},
247  year      = {1994},
248  pages     = {245-296},
249  ee        = {http://dx.doi.org/10.1006/inco.1994.1046},
250  bibsource = {DBLP, http://dblp.uni-trier.de}
251}
252
253@article{stateart,
254  author    = {Reinhard Wilhelm and
255               Jakob Engblom and
256               Andreas Ermedahl and
257               Niklas Holsti and
258               Stephan Thesing and
259               David B. Whalley and
260               Guillem Bernat and
261               Christian Ferdinand and
262               Reinhold Heckmann and
263               Tulika Mitra and
264               Frank Mueller and
265               Isabelle Puaut and
266               Peter P. Puschner and
267               Jan Staschulat and
268               Per Stenstr{\"o}m},
269  title     = {The worst-case execution-time problem---overview of methods
270               and survey of tools},
271  journal   = {ACM Trans. Embedded Comput. Syst.},
272  volume    = {7},
273  number    = {3},
274  year      = {2008},
275  ee        = {http://doi.acm.org/10.1145/1347375.1347389},
276  bibsource = {DBLP, http://dblp.uni-trier.de}
277}
278
279@inproceedings{bobot,
280  year={2012},
281  booktitle={Formal Methods and Software Engineering},
282  volume={7635},
283  series={Lecture Notes in Computer Science},
284  doi={10.1007/978-3-642-34281-3_14},
285  title={Separation Predicates: A Taste of Separation Logic in First-Order Logic},
286  url={http://dx.doi.org/10.1007/978-3-642-34281-3_14},
287  author={Bobot, François and Filliâtre, Jean-Christophe},
288  pages={167-181}
289}
290
291@misc
292{ absint,
293  url = {http://www.absint.com/ait/},
294  author = {{AbsInt}},
295  title = {{aiT WCET} analysis tools}
296}
297
298@misc
299{ cerco-website,
300  url = {http://cerco.cs.unibo.it},
301  title = {The {Certified Complexity} ({CerCo}) project web site},
302  key = {cerco}
303}
304
305@misc
306{ jessie,
307  url = {http://krakatoa.lri.fr/},
308  title = {Jessie {Frama-C} plugin},
309  key = {jessie}
310}
311
312@article
313{ asperti:user:2007,
314  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
315  title = {User interaction with the {Matita} proof assistant},
316  journal = {Automated Reasoning},
317  pages = {109--139},
318  volume = {39},
319  issue = {2},
320  year = {2007}
321}
322
323@article
324{ sacerdoti-coen:tinycals:2007,
325  author = {Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
326  title = {{Tinycals}: Step by Step Tacticals},
327  journal = {Electronic Notes in Theoretical Computer Science},
328  volume = {174},
329  number = {2},
330  pages = {125--142},
331  doi = {http://dx.doi.org/10.1016/j.entcs.2006.09.026},
332  year = {2007}
333}
334
335@incollection
336{ sozeau:subset:2007,
337  author = {Matthieu Sozeau},
338  title = {Subset Coercions in {Coq}},
339  booktitle = {Types for Proofs and Programs},
340  volume = {4502},
341  series = {Lecture Notes in Computer Science},
342  doi = {10.1007/978-3-540-74464-1_16},
343  pages = {237--252},
344  year = {2007}
345}
346
347@inproceedings
348{ asperti:higher-order:2007,
349  author = {Andrea Asperti and Enrico Tassi},
350  title = {Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case},
351  booktitle = {Towards Mechanized Mathematical Assistants: Calculemus},
352  pages = {146--160},
353  series = {Lecture Notes in Computer Science},
354  volume = {4573},
355  year = 2007
356}
357
358@inproceedings
359{ bove:brief:2009,
360  author = {Ana Bove and Peter Dybjer and Ulf Norell},
361  title = {A Brief Overview of {Agda} --- A Functional Language with Dependent Types},
362  booktitle = {Theorem Proving in Higher-order Logics {(TPHOLs)}},
363  year = {2009}
364}
365
366@manual
367{ coq:2004,
368  title = {The {Coq} proof assistant reference manual},
369  author =  {{The Coq development team}},
370  organization = {{LogiCal Project}},
371  note = {Version 8.0},
372  year = {2004},
373  url = {http://coq.inria.fr}
374}
375
376@misc
377{ cerco:2011,
378  title = {The {CerCo} {FET-Open} project},
379  howpublished = {\url{http://cerco.cs.unibo.it/}},
380  year = {2011},
381  key = {CerCo:2011}
382}
383
384@inproceedings{cil02,
385  title  = {{CIL}: Intermediate Language and Tools for Analysis and Transformation of {C} Programs},
386  author = {George C. Necula and Scott McPeak and Shree P. Rahul and Westley Weimer},
387  booktitle = {Compiler Construction: 11th International Conference (CC 2002)},
388  pages = {213--228},
389  year   = 2002,
390  editor = {R. Nigel Horspool},
391  volume = 2304,
392  series = {Lecture Notes in Computer Science},
393  publisher = {Springer},
394  doi = {10.1007/3-540-45937-5_16}
395}
Note: See TracBrowser for help on using the repository browser.