source: Papers/fopara2013/fopara13.bib @ 3455

Last change on this file since 3455 was 3455, checked in by mulligan, 6 years ago

more space saving. now down to 16 pages + 1 page bibliography

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. 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{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@Unpublished{paolo,
84 author = {Paolo Tranquilli},
85 title = {Indexed Labels for Loop Iteration Dependent Costs},
86 note = {to appear in EPTCS, proceedings of QAPL 2013},
87 month = jan,
88 year = {2013},
89 url = {http://www.cs.unibo.it/~tranquil/content/docs/indlabels.pdf}
90}
91
92@INPROCEEDINGS{separation,
93    author = {John C. Reynolds},
94    title = {Intuitionistic Reasoning about Shared Mutable Data Structure},
95    booktitle = {Millennial Perspectives in Computer Science},
96    year = {2000},
97    pages = {303--321},
98    publisher = {Palgrave}
99}
100
101@inproceedings{lustre,
102  author    = {Paul Caspi and
103               Daniel Pilaud and
104               Nicolas Halbwachs and
105               John Plaice},
106  title     = {Lustre: A Declarative Language for Programming Synchronous
107               Systems},
108  booktitle = {POPL},
109  year      = {1987},
110  pages     = {178-188},
111  ee        = {http://doi.acm.org/10.1145/41625.41641},
112  crossref  = {DBLP:conf/popl/1987},
113  bibsource = {DBLP, http://dblp.uni-trier.de}
114}
115@proceedings{DBLP:conf/popl/1987,
116  title     = {Conference Record of the Fourteenth Annual ACM Symposium
117               on Principles of Programming Languages, Munich, Germany,
118               January 21-23, 1987},
119  booktitle = {POPL},
120  publisher = {ACM Press},
121  year      = {1987},
122  isbn      = {0-89791-215-2},
123  ee        = {http://dl.acm.org/citation.cfm?id=41625},
124  bibsource = {DBLP, http://dblp.uni-trier.de}
125}
126 
127@inproceedings{correctness,
128  author    = {Mulligan, Dominic P.  and
129               Sacerdoti Coen, Claudio},
130  title     = {On the Correctness of an Optimising Assembler for the {Intel
131               MCS-51} Microprocessor},
132  booktitle = {CPP},
133  year      = {2012},
134  pages     = {43--59},
135  doi       = {10.1007/978-3-642-35308-6_7}
136}
137@proceedings{DBLP:conf/cpp/2012,
138  editor    = {Chris Hawblitzel and
139               Dale Miller},
140  title     = {Certified Programs and Proofs - Second International Conference,
141               CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
142  booktitle = {CPP},
143  publisher = {Springer},
144  series    = {LNCS},
145  volume    = {7679},
146  year      = {2012},
147  isbn      = {978-3-642-35307-9},
148  ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6},
149  bibsource = {DBLP, http://dblp.uni-trier.de}
150}
151
152@article{proartis,
153    title = {PROARTIS: Probabilistically Analysable Real-Time Systems},
154    journal = {Transactions on Embedded Computing Systems},
155    year = {2012},
156    publisher = {ACM},
157    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}
158}
159
160@inproceedings{embounded,
161  author    = {Kevin Hammond and
162               Roy Dyckhoff and
163               Christian Ferdinand and
164               Reinhold Heckmann and
165               Martin Hofmann and
166               Steffen Jost and
167               Hans-Wolfgang Loidl and
168               Greg Michaelson and
169               Robert F. Pointon and
170               Norman Scaife and
171               Jocelyn S{\'e}rot and
172               Andy Wallace},
173  title     = {{The {EmBounded} Project (Project Start Paper)}},
174  booktitle = {TFP},
175  year      = {2005},
176  pages     = {195--210},
177  crossref  = {TFP2005},
178}
179
180@proceedings{TFP2005,
181  title     = {Revised Selected Papers from the Sixth Symposium on Trends
182               in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
183               September 2005},
184  booktitle = {Trends in Functional Programming},
185  series    = {Trends in Functional Programming},
186  volume    = {6},
187  year      = {2007},
188  isbn      = {978-1-84150-176-5},
189}
190
191@inproceedings{matita,
192  author    = {Andrea Asperti and
193               Wilmer Ricciotti and
194               Claudio Sacerdoti Coen and
195               Enrico Tassi},
196  title     = {The {Matita} Interactive Theorem Prover},
197  booktitle = {CADE},
198  year      = {2011},
199  pages     = {64-69},
200  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6_7},
201  crossref  = {DBLP:conf/cade/2011},
202  bibsource = {DBLP, http://dblp.uni-trier.de}
203}
204@proceedings{DBLP:conf/cade/2011,
205  title     = {Automated Deduction - CADE-23 - 23rd International Conference
206               on Automated Deduction, Wroclaw, Poland, July 31 - August
207               5, 2011. Proceedings},
208  booktitle = {CADE},
209  publisher = {Springer},
210  series    = {LNCS},
211  volume    = {6803},
212  year      = {2011},
213  isbn      = {978-3-642-22437-9},
214  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6},
215  bibsource = {DBLP, http://dblp.uni-trier.de}
216}
217
218@article{typeffects,
219  author    = {Jean-Pierre Talpin and
220               Pierre Jouvelot},
221  title     = {The Type and Effect Discipline},
222  journal   = {Inf. Comput.},
223  volume    = {111},
224  number    = {2},
225  year      = {1994},
226  pages     = {245-296},
227  ee        = {http://dx.doi.org/10.1006/inco.1994.1046},
228  bibsource = {DBLP, http://dblp.uni-trier.de}
229}
230
231@article{stateart,
232  author    = {Reinhard Wilhelm and
233               Jakob Engblom and
234               Andreas Ermedahl and
235               Niklas Holsti and
236               Stephan Thesing and
237               David B. Whalley and
238               Guillem Bernat and
239               Christian Ferdinand and
240               Reinhold Heckmann and
241               Tulika Mitra and
242               Frank Mueller and
243               Isabelle Puaut and
244               Peter P. Puschner and
245               Jan Staschulat and
246               Per Stenstr{\"o}m},
247  title     = {The worst-case execution-time problem - overview of methods
248               and survey of tools},
249  journal   = {ACM Trans. Embedded Comput. Syst.},
250  volume    = {7},
251  number    = {3},
252  year      = {2008},
253  ee        = {http://doi.acm.org/10.1145/1347375.1347389},
254  bibsource = {DBLP, http://dblp.uni-trier.de}
255}
256
257@inproceedings{bobot,
258  year={2012},
259  isbn={978-3-642-34280-6},
260  booktitle={Formal Methods and Software Engineering},
261  volume={7635},
262  series={Lecture Notes in Computer Science},
263  editor={Aoki, Toshiaki and Taguchi, Kenji},
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  publisher={Springer Berlin Heidelberg},
268  author={Bobot, François and Filliâtre, Jean-Christophe},
269  pages={167-181}
270}
271
272@misc
273{ absint,
274  url = {http://www.absint.com/ait/},
275  author = {{AbsInt}},
276  title = {{aiT WCET} analysis tools}
277}
278
279@misc
280{ cerco-deliverables,
281  url = {http://cerco.cs.unibo.it},
282  title = {The {Certified Complexity} ({CerCo}) project papers and deliverables},
283  key = {cerco}
284}
285
286@misc
287{ jessie,
288  url = {http://krakatoa.lri.fr/},
289  title = {Jessie {Frama-C} plugin},
290  key = {jessie}
291}
Note: See TracBrowser for help on using the repository browser.