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, |
---|
28 | year={2012}, |
---|
29 | isbn={978-3-642-32468-0}, |
---|
30 | booktitle={Formal Methods for Industrial Critical Systems}, |
---|
31 | volume={7437}, |
---|
32 | series={LNCS}, |
---|
33 | doi={10.1007/978-3-642-32469-7_3}, |
---|
34 | title={Certifying and Reasoning on Cost Annotations in {C} Programs}, |
---|
35 | url={http://dx.doi.org/10.1007/978-3-642-32469-7_3}, |
---|
36 | author={Ayache, Nicolas and Amadio, Roberto and R\'egis-Gianas, Yann}, |
---|
37 | pages={32--46}, |
---|
38 | publisher={Springer Berlin Heidelberg} |
---|
39 | } |
---|
40 | |
---|
41 | @incollection{labelling2, |
---|
42 | year={2012}, |
---|
43 | booktitle={Foundational and Practical Aspects of Resource Analysis}, |
---|
44 | volume={7177}, |
---|
45 | series={LNCS}, |
---|
46 | doi={10.1007/978-3-642-32495-6_5}, |
---|
47 | title={Certifying and Reasoning on Cost Annotations of Functional Programs}, |
---|
48 | author={Amadio, Roberto and R\'egis-Gianas, Yann}, |
---|
49 | pages={72--89}, |
---|
50 | note={Extended version to appear in Higher Order and Symbolic Computation}, |
---|
51 | publisher={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 |
---|
67 | of semantic preservation) of CompCert, a compiler from Clight (a |
---|
68 | large subset of the C programming language) to PowerPC assembly code, |
---|
69 | using the Coq proof assistant both for programming the compiler and |
---|
70 | for proving its correctness. Such a verified compiler is useful in |
---|
71 | the context of critical software and its formal verification: the |
---|
72 | verification of the compiler guarantees that the safety properties |
---|
73 | proved on the source code hold for the executable compiled code as |
---|
74 | well.} |
---|
75 | } |
---|
76 | |
---|
77 | @Manual{framac, |
---|
78 | title = {Frama-{C} user manual}, |
---|
79 | author = {L. Correnson and P. Cuoq and F. Kirchner and V. Prevosto and A. Puccetti and J. Signoles and |
---|
80 | B. Yakobowski}, |
---|
81 | organization = {CEA-LIST, Software Safety Laboratory, Saclay, F-91191}, |
---|
82 | note = {\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 | } |
---|
293 | |
---|
294 | @article |
---|
295 | { asperti:user:2007, |
---|
296 | author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli}, |
---|
297 | title = {User interaction with the {Matita} proof assistant}, |
---|
298 | journal = {Automated Reasoning}, |
---|
299 | pages = {109--139}, |
---|
300 | volume = {39}, |
---|
301 | issue = {2}, |
---|
302 | year = {2007} |
---|
303 | } |
---|
304 | |
---|
305 | @article |
---|
306 | { sacerdoti-coen:tinycals:2007, |
---|
307 | author = {Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli}, |
---|
308 | title = {{Tinycals}: Step by Step Tacticals}, |
---|
309 | journal = {Electronic Notes in Theoretical Computer Science}, |
---|
310 | volume = {174}, |
---|
311 | number = {2}, |
---|
312 | pages = {125--142}, |
---|
313 | doi = {http://dx.doi.org/10.1016/j.entcs.2006.09.026}, |
---|
314 | year = {2007} |
---|
315 | } |
---|
316 | |
---|
317 | @incollection |
---|
318 | { sozeau:subset:2007, |
---|
319 | author = {Matthieu Sozeau}, |
---|
320 | title = {Subset Coercions in {Coq}}, |
---|
321 | booktitle = {Types for Proofs and Programs}, |
---|
322 | volume = {4502}, |
---|
323 | series = {Lecture Notes in Computer Science}, |
---|
324 | doi = {10.1007/978-3-540-74464-1_16}, |
---|
325 | pages = {237--252}, |
---|
326 | year = {2007} |
---|
327 | } |
---|
328 | |
---|
329 | @inproceedings |
---|
330 | { asperti:higher-order:2007, |
---|
331 | author = {Andrea Asperti and Enrico Tassi}, |
---|
332 | title = {Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case}, |
---|
333 | booktitle = {Towards Mechanized Mathematical Assistants: Calculemus}, |
---|
334 | pages = {146--160}, |
---|
335 | series = {Lecture Notes in Computer Science}, |
---|
336 | volume = {4573}, |
---|
337 | year = 2007 |
---|
338 | } |
---|
339 | |
---|
340 | @inproceedings |
---|
341 | { bove:brief:2009, |
---|
342 | author = {Ana Bove and Peter Dybjer and Ulf Norell}, |
---|
343 | title = {A Brief Overview of {Agda} --- A Functional Language with Dependent Types}, |
---|
344 | booktitle = {Theorem Proving in Higher-order Logics {(TPHOLs)}}, |
---|
345 | year = {2009} |
---|
346 | } |
---|
347 | |
---|
348 | @manual |
---|
349 | { coq:2004, |
---|
350 | title = {The {Coq} proof assistant reference manual}, |
---|
351 | author = {{The Coq development team}}, |
---|
352 | organization = {{LogiCal Project}}, |
---|
353 | note = {Version 8.0}, |
---|
354 | year = {2004}, |
---|
355 | url = {http://coq.inria.fr} |
---|
356 | } |
---|
357 | |
---|
358 | @misc |
---|
359 | { cerco:2011, |
---|
360 | title = {The {CerCo} {FET-Open} project}, |
---|
361 | howpublished = {\url{http://cerco.cs.unibo.it/}}, |
---|
362 | year = {2011}, |
---|
363 | key = {CerCo:2011} |
---|
364 | } |
---|