source: Papers/fopara2013/fopara13.bib @ 3462

Last change on this file since 3462 was 3462, checked in by campbell, 6 years ago

Some final changes before submission.

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