source: Papers/fopara2013/fopara13.bib @ 3368

Last change on this file since 3368 was 3339, checked in by tranquil, 6 years ago

passed biblio to bibtex, and some aesthetical changes

File size: 9.1 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. 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 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{labeling,
28year={2012},
29isbn={978-3-642-32468-0},
30booktitle={Formal Methods for Industrial Critical Systems},
31volume={7437},
32series={LNCS},
33editor={Stoelinga, Mariëlle and Pinger, Ralf},
34doi={10.1007/978-3-642-32469-7_3},
35title={Certifying and Reasoning on Cost Annotations in {C} Programs},
36url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
37publisher={Springer Berlin Heidelberg},
38author={Ayache, Nicolas and Amadio, RobertoM. and R\'egis-Gianas, Yann},
39pages={32-46}
40}
41
42@incollection{labeling2,
43year={2012},
44isbn={978-3-642-32494-9},
45booktitle={Foundational and Practical Aspects of Resource Analysis},
46volume={7177},
47series={LNCS},
48editor={Peña, Ricardo and Eekelen, Marko and Shkaravska, Olha},
49doi={10.1007/978-3-642-32495-6_5},
50title={Certifying and Reasoning on Cost Annotations of Functional Programs},
51url={http://dx.doi.org/10.1007/978-3-642-32495-6_5},
52publisher={Springer Berlin Heidelberg},
53author={Amadio, RobertoM. and R\'egis-Gianas, Yann},
54pages={72-89},
55note={Extended version to appear in Higher Order and Symbolic Computation, 2013}
56}
57
58@article{compcert,
59  author = {Xavier Leroy},
60  title = {Formal verification of a realistic compiler},
61  journal = {Communications of the ACM},
62  year = 2009,
63  volume = 52,
64  number = 7,
65  pages = {107--115},
66  url = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
67  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
68  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
69  pubkind = {journal-int-mono},
70  abstract = {This paper reports on the development and formal verification (proof
71of semantic preservation) of CompCert, a compiler from Clight (a
72large subset of the C programming language) to PowerPC assembly code,
73using the Coq proof assistant both for programming the compiler and
74for proving its correctness.  Such a verified compiler is useful in
75the context of critical software and its formal verification: the
76verification of the compiler guarantees that the safety properties
77proved on the source code hold for the executable compiled code as
78well.}
79}
80
81@Manual{framac,
82title = {Frama-{C} user manual},
83author = {L. Correnson and P. Cuoq and F. Kirchner and V. Prevosto and A. Puccetti and J. Signoles and
84B. Yakobowski},
85organization = {CEA-LIST, Software Safety Laboratory, Saclay, F-91191},
86note = {\url{http://frama-c.com/}}
87}
88
89@Unpublished{paolo,
90 author = {Paolo Tranquilli},
91 title = {Indexed Labels for Loop Iteration Dependent Costs},
92 note = {to appear in EPTCS, proceedings of QAPL 2013},
93 month = jan,
94 year = {2013},
95 url = {http://www.cs.unibo.it/~tranquil/content/docs/indlabels.pdf}
96}
97
98@INPROCEEDINGS{separation,
99    author = {John C. Reynolds},
100    title = {Intuitionistic Reasoning about Shared Mutable Data Structure},
101    booktitle = {Millennial Perspectives in Computer Science},
102    year = {2000},
103    pages = {303--321},
104    publisher = {Palgrave}
105}
106
107@inproceedings{lustre,
108  author    = {Paul Caspi and
109               Daniel Pilaud and
110               Nicolas Halbwachs and
111               John Plaice},
112  title     = {Lustre: A Declarative Language for Programming Synchronous
113               Systems},
114  booktitle = {POPL},
115  year      = {1987},
116  pages     = {178-188},
117  ee        = {http://doi.acm.org/10.1145/41625.41641},
118  crossref  = {DBLP:conf/popl/1987},
119  bibsource = {DBLP, http://dblp.uni-trier.de}
120}
121@proceedings{DBLP:conf/popl/1987,
122  title     = {Conference Record of the Fourteenth Annual ACM Symposium
123               on Principles of Programming Languages, Munich, Germany,
124               January 21-23, 1987},
125  booktitle = {POPL},
126  publisher = {ACM Press},
127  year      = {1987},
128  isbn      = {0-89791-215-2},
129  ee        = {http://dl.acm.org/citation.cfm?id=41625},
130  bibsource = {DBLP, http://dblp.uni-trier.de}
131}
132 
133@inproceedings{correctness,
134  author    = {Mulligan, Dominic P.  and
135               Sacerdoti Coen, Claudio},
136  title     = {On the Correctness of an Optimising Assembler for the Intel
137               MCS-51 Microprocessor},
138  booktitle = {CPP},
139  year      = {2012},
140  pages     = {43-59},
141  ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6_7},
142  crossref  = {DBLP:conf/cpp/2012},
143  bibsource = {DBLP, http://dblp.uni-trier.de}
144}
145@proceedings{DBLP:conf/cpp/2012,
146  editor    = {Chris Hawblitzel and
147               Dale Miller},
148  title     = {Certified Programs and Proofs - Second International Conference,
149               CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
150  booktitle = {CPP},
151  publisher = {Springer},
152  series    = {LNCS},
153  volume    = {7679},
154  year      = {2012},
155  isbn      = {978-3-642-35307-9},
156  ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6},
157  bibsource = {DBLP, http://dblp.uni-trier.de}
158}
159
160@article{proartis,
161    title = {PROARTIS: Probabilistically Analysable Real-Time Systems},
162    journal = {Transactions on Embedded Computing Systems},
163    year = {2012},
164    publisher = {ACM},
165    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}
166}
167
168@inproceedings{embounded,
169  author    = {Kevin Hammond and
170               Roy Dyckhoff and
171               Christian Ferdinand and
172               Reinhold Heckmann and
173               Martin Hofmann and
174               Steffen Jost and
175               Hans-Wolfgang Loidl and
176               Greg Michaelson and
177               Robert F. Pointon and
178               Norman Scaife and
179               Jocelyn S{\'e}rot and
180               Andy Wallace},
181  title     = {{The Embounded Project (Project Start Paper)}},
182  booktitle = {TFP},
183  year      = {2005},
184  pages     = {195--210},
185  crossref  = {TFP2005},
186}
187
188@proceedings{TFP2005,
189  title     = {Revised Selected Papers from the Sixth Symposium on Trends
190               in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
191               September 2005},
192  booktitle = {Trends in Functional Programming},
193  publisher = {Intellect, UK/The University of Chicago Press, USA},
194  series    = {Trends in Functional Programming},
195  volume    = {6},
196  year      = {2007},
197  isbn      = {978-1-84150-176-5},
198}
199
200@inproceedings{matita,
201  author    = {Andrea Asperti and
202               Wilmer Ricciotti and
203               Claudio Sacerdoti Coen and
204               Enrico Tassi},
205  title     = {The Matita Interactive Theorem Prover},
206  booktitle = {CADE},
207  year      = {2011},
208  pages     = {64-69},
209  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6_7},
210  crossref  = {DBLP:conf/cade/2011},
211  bibsource = {DBLP, http://dblp.uni-trier.de}
212}
213@proceedings{DBLP:conf/cade/2011,
214  title     = {Automated Deduction - CADE-23 - 23rd International Conference
215               on Automated Deduction, Wroclaw, Poland, July 31 - August
216               5, 2011. Proceedings},
217  booktitle = {CADE},
218  publisher = {Springer},
219  series    = {LNCS},
220  volume    = {6803},
221  year      = {2011},
222  isbn      = {978-3-642-22437-9},
223  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6},
224  bibsource = {DBLP, http://dblp.uni-trier.de}
225}
226
227@article{typeffects,
228  author    = {Jean-Pierre Talpin and
229               Pierre Jouvelot},
230  title     = {The Type and Effect Discipline},
231  journal   = {Inf. Comput.},
232  volume    = {111},
233  number    = {2},
234  year      = {1994},
235  pages     = {245-296},
236  ee        = {http://dx.doi.org/10.1006/inco.1994.1046},
237  bibsource = {DBLP, http://dblp.uni-trier.de}
238}
239
240@article{stateart,
241  author    = {Reinhard Wilhelm and
242               Jakob Engblom and
243               Andreas Ermedahl and
244               Niklas Holsti and
245               Stephan Thesing and
246               David B. Whalley and
247               Guillem Bernat and
248               Christian Ferdinand and
249               Reinhold Heckmann and
250               Tulika Mitra and
251               Frank Mueller and
252               Isabelle Puaut and
253               Peter P. Puschner and
254               Jan Staschulat and
255               Per Stenstr{\"o}m},
256  title     = {The worst-case execution-time problem - overview of methods
257               and survey of tools},
258  journal   = {ACM Trans. Embedded Comput. Syst.},
259  volume    = {7},
260  number    = {3},
261  year      = {2008},
262  ee        = {http://doi.acm.org/10.1145/1347375.1347389},
263  bibsource = {DBLP, http://dblp.uni-trier.de}
264}
Note: See TracBrowser for help on using the repository browser.