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

Last change on this file was 3666, checked in by boender, 3 years ago

Updated the proof part

File size: 65.3 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  url       = {http://doi.acm.org/10.1145/2594291.2594301},
19  doi       = {10.1145/2594291.2594301},
20  timestamp = {Tue, 20 Dec 2016 10:12:01 +0100},
21  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/pldi/Carbonneaux0RS14},
22  bibsource = {dblp computer science bibliography, http://dblp.org}
23}
24
25@misc { stackanalyzer,
26  title = {{AbsInt} {Gmbh} {StackAnalyzer} stack space analysis tool},
27  url = {https://www.absint.com/stackanalyzer/index.htm},
28  note = {Accessed March 2017},
29  year = {2017},
30  key = {stackanalyzer}
31}
32
33@phdthesis{Hoffmann11,
34  author = {Jan Hoffmann},
35  title = {{Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis}},
36  school = {Ludwig-Maximilians-Universi{\"a}t M{\"u}nchen},
37  year =  2011
38}
39
40@inproceedings{Tristan-Leroy-LCM,
41  author = {Jean-Baptiste Tristan and Xavier Leroy},
42  title = {Verified Validation of {Lazy} {Code} {Motion}},
43  booktitle = {Proceedings of the 2009 ACM SIGPLAN Conference on
44                         Programming Language Design and Implementation
45                         (PLDI'09)},
46  year = 2009,
47  pages = {316--326},
48  url = {http://gallium.inria.fr/~xleroy/publi/validation-LCM.pdf},
49  urlpublisher = {http://doi.acm.org/10.1145/1542476.1542512},
50  hal = {http://hal.archives-ouvertes.fr/inria-00415865/},
51  pubkind = {conf-int-mono}
52}
53
54@incollection{Leroy-Appel-Blazy-Stewart-memory,
55  author = {Leroy, Xavier and Appel, Andrew W. and Blazy, Sandrine and Stewart, Gordon},
56  title = {The {CompCert} memory model},
57  year = {2014},
58  month = apr,
59  booktitle = {Program Logics for Certified Compilers},
60  editor = {Appel, Andrew W.},
61  publisher = {Cambridge University Press},
62  url = {http://vst.cs.princeton.edu/}
63}
64
65@article{Sevcik:2013:CVC:2487241.2487248,
66 author = {\v{S}ev\v{c}\'{\i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
67 title = {CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency},
68 journal = {J. ACM},
69 issue_date = {June 2013},
70 volume = {60},
71 number = {3},
72 month = jun,
73 year = {2013},
74 issn = {0004-5411},
75 pages = {22:1--22:50},
76 articleno = {22},
77 numpages = {50},
78 url = {http://doi.acm.org/10.1145/2487241.2487248},
79 doi = {10.1145/2487241.2487248},
80 acmid = {2487248},
81 publisher = {ACM},
82 address = {New York, NY, USA},
83 keywords = {Relaxed memory models, semantics, verified compilation},
84} 
85
86@article{Kang:2016:LVS:2914770.2837642,
87 author = {Kang, Jeehoon and Kim, Yoonseung and Hur, Chung-Kil and Dreyer, Derek and Vafeiadis, Viktor},
88 title = {Lightweight Verification of Separate Compilation},
89 journal = {SIGPLAN Not.},
90 issue_date = {January 2016},
91 volume = {51},
92 number = {1},
93 month = jan,
94 year = {2016},
95 issn = {0362-1340},
96 pages = {178--190},
97 numpages = {13},
98 url = {http://doi.acm.org/10.1145/2914770.2837642},
99 doi = {10.1145/2914770.2837642},
100 acmid = {2837642},
101 publisher = {ACM},
102 address = {New York, NY, USA},
103 keywords = {CompCert, Compositional compiler verification, separate compilation},
104}
105
106@Inbook{Atkey2010,
107author="Atkey, Robert",
108editor="Gordon, Andrew D.",
109title="Amortised Resource Analysis with Separation Logic",
110bookTitle="Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings",
111year="2010",
112publisher="Springer Berlin Heidelberg",
113address="Berlin, Heidelberg",
114pages="85--103",
115isbn="978-3-642-11957-6",
116doi="10.1007/978-3-642-11957-6_6",
117url="http://dx.doi.org/10.1007/978-3-642-11957-6_6"
118}
119
120
121@Inbook{Aspinall2010,
122author="Aspinall, David
123and Atkey, Robert
124and MacKenzie, Kenneth
125and Sannella, Donald",
126editor="Wirsing, Martin
127and Hofmann, Martin
128and Rauschmayer, Axel",
129title="Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode",
130bookTitle="Trustworthly Global Computing: 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers",
131year="2010",
132publisher="Springer Berlin Heidelberg",
133address="Berlin, Heidelberg",
134pages="1--22",
135isbn="978-3-642-15640-3",
136doi="10.1007/978-3-642-15640-3_1",
137url="http://dx.doi.org/10.1007/978-3-642-15640-3_1"
138}
139
140
141@article{Salvucci201627,
142title = "Memory Consumption Analysis for a Functional and Imperative Language ",
143journal = "Electronic Notes in Theoretical Computer Science ",
144volume = "330",
145number = "",
146pages = "27 - 46",
147year = "2016",
148note = "\{RAC\} 2016 - Resource Aware Computing ",
149issn = "1571-0661",
150doi = "http://dx.doi.org/10.1016/j.entcs.2016.12.013",
151url = "http://www.sciencedirect.com/science/article/pii/S1571066116301207",
152author = "Jérémie Salvucci and Emmanuel Chailloux",
153keywords = "ML",
154keywords = "regions",
155keywords = "static analysis",
156keywords = "memory analysis ",
157abstract = "Abstract The omnipresence of resource-constrained embedded systems makes them critical components. Programmers have to provide strong guarantees about their runtime behavior to make them reliable. Among these, giving an upper bound of live memory at runtime is mandatory to prevent heap overflows from happening. The paper proposes a semi-automatic technique to infer the space complexity of ML-like programs with explicit region management. It aims at combining existing formalisms to obtain the space complexity of imperative and purely functional programs in a consistent framework. "
158}
159
160
161@Inbook{Hoffmann2015,
162author="Hoffmann, Jan
163and Shao, Zhong",
164editor="Vitek, Jan",
165title="Automatic Static Cost Analysis for Parallel Programs",
166bookTitle="Programming Languages and Systems: 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings",
167year="2015",
168publisher="Springer Berlin Heidelberg",
169address="Berlin, Heidelberg",
170pages="132--157",
171isbn="978-3-662-46669-8",
172doi="10.1007/978-3-662-46669-8_6",
173url="http://dx.doi.org/10.1007/978-3-662-46669-8_6"
174}
175
176
177@inproceedings{HAH12,
178  author    = {Jan Hoffmann and Klaus Aehlig and
179               Martin Hofmann},
180  title     = {{Resource Aware ML}},
181  booktitle = {{24rd International Conference on Computer Aided
182                  Verification (CAV'12)}},
183  publisher = {Springer},
184  series    = {Lecture Notes in Computer Science},
185  volume    = {7358},
186  pages     = {781-786},
187  year      = {2012}
188}
189
190@article{Stewart:2015:CC:2775051.2676985,
191 author = {Stewart, Gordon and Beringer, Lennart and Cuellar, Santiago and Appel, Andrew W.},
192 title = {Compositional CompCert},
193 journal = {SIGPLAN Not.},
194 issue_date = {January 2015},
195 volume = {50},
196 number = {1},
197 month = jan,
198 year = {2015},
199 issn = {0362-1340},
200 pages = {275--287},
201 numpages = {13},
202 url = {http://doi.acm.org/10.1145/2775051.2676985},
203 doi = {10.1145/2775051.2676985},
204 acmid = {2676985},
205 publisher = {ACM},
206 address = {New York, NY, USA},
207 keywords = {compcert, compiler correctness},
208} 
209
210@inproceedings{Boldo-Jourdan-Leroy-Melquiond-2013,
211  title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
212  author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
213  booktitle = {ARITH, 21st IEEE International Symposium on Computer Arithmetic},
214  pages = {107-115},
215  publisher = {IEEE Computer Society Press},
216  url = {http://hal.inria.fr/hal-00743090},
217  year = 2013,
218  xtopic = {compcert},
219  abstract = {Floating-point arithmetic is known to be tricky: roundings, formats,
220exceptional values. The IEEE-754 standard was a push towards
221straightening the field and made formal reasoning about floating-point
222computations easier and flourishing. Unfortunately, this is not
223sufficient to guarantee the final result of a program, as several
224other actors are involved: programming language, compiler,
225architecture.  The CompCert formally-verified compiler provides a
226solution to this problem: this compiler comes with a mathematical
227specification of the semantics of its source language (a large subset
228of ISO C90) and target platforms (ARM, PowerPC, x86-SSE2), and with a
229proof that compilation preserves semantics.  In this paper, we report
230on our recent success in formally specifying and proving correct
231CompCert's compilation of floating-point arithmetic.  Since CompCert
232is verified using the Coq proof assistant, this effort required a
233suitable Coq formalization of the IEEE-754 standard; we extended the
234Flocq library for this purpose.  As a result, we obtain the first
235formally verified compiler that provably preserves the semantics of
236floating-point programs.}
237}
238
239@inproceedings{2006-Leroy-Bertot-Gregoire,
240  author = {Yves Bertot and Benjamin Grégoire and Xavier Leroy},
241  title = {A structured approach to proving compiler
242                         optimizations based on dataflow analysis},
243  booktitle = {Types for Proofs and Programs, Workshop TYPES 2004},
244  year = 2006,
245  volume = 3839,
246  pages = {66-81},
247  series = {Lecture Notes in Computer Science},
248  publisher = {Springer},
249  url = {http://gallium.inria.fr/~xleroy/publi/proofs_dataflow_optimizations.pdf},
250  urlpublisher = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11617990_5},
251  hal = {http://hal.inria.fr/inria-00289549/},
252  abstract = {
253This paper reports on the correctness proof of compiler optimizations
254based on data-flow analysis.  We formulate the optimizations and
255analyses as instances of a general framework for data-flow analyses and
256transformations, and prove that the optimizations preserve the
257behavior of the compiled programs.  This development is a part of a
258larger effort of certifying an optimizing compiler by proving semantic
259equivalence between source and compiled code.}
260}
261
262@inproceedings{Robert-Leroy-2012,
263  author = {Valentin Robert and Xavier Leroy},
264  title = {A Formally-Verified Alias Analysis},
265  booktitle = {Certified Programs and Proofs (CPP 2012)},
266  year = 2012,
267  series = {Lecture Notes in Computer Science},
268  volume = 7679,
269  pages = {11-26},
270  publisher = {Springer},
271  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-35308-6_5},
272  url = {http://gallium.inria.fr/~xleroy/publi/alias-analysis.pdf},
273  xtopic = {compcert},
274  abstract = {This paper reports on the formalization and proof of soundness, using
275the Coq proof assistant, of an alias analysis: a static analysis that
276approximates the flow of pointer values.  The alias analysis
277considered is of the points-to kind and is intraprocedural,
278flow-sensitive, field-sensitive, and untyped.  Its soundness proof
279follows the general style of abstract interpretation.
280The analysis is designed to fit in the CompCert C verified compiler,
281supporting future aggressive optimizations over memory accesses.}
282}
283
284@article{LEINENBACH200823,
285title = "Pervasive Compiler Verification – From Verified Programs to Verified Systems",
286journal = "Electronic Notes in Theoretical Computer Science",
287volume = "217",
288number = "",
289pages = "23 - 40",
290year = "2008",
291note = "",
292issn = "1571-0661",
293doi = "http://dx.doi.org/10.1016/j.entcs.2008.06.040",
294url = "http://www.sciencedirect.com/science/article/pii/S1571066108003836",
295author = "Dirk Leinenbach and Elena Petrova",
296keywords = "Compiler Verification",
297keywords = "Theorem Proving",
298keywords = "System Verification",
299keywords = "HOL",
300keywords = "Hoare Logic"
301}
302
303@inproceedings{DBLP:conf/cpp/MulliganC12,
304  author    = {Dominic P. Mulligan and
305               Claudio Sacerdoti Coen},
306  title     = {On the Correctness of an Optimising Assembler for the Intel {MCS-51}
307               Microprocessor},
308  booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
309               2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
310  pages     = {43--59},
311  year      = {2012},
312  url       = {http://dx.doi.org/10.1007/978-3-642-35308-6_7},
313  doi       = {10.1007/978-3-642-35308-6_7},
314  timestamp = {Thu, 08 Nov 2012 16:22:09 +0100},
315  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/MulliganC12},
316  bibsource = {dblp computer science bibliography, http://dblp.org}
317}
318
319@inproceedings{DBLP:conf/tacas/BoenderC14,
320  author    = {Jaap Boender and
321               Claudio Sacerdoti Coen},
322  title     = {On the Correctness of a Branch Displacement Algorithm},
323  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
324               - 20th International Conference, {TACAS} 2014, Held as Part of the
325               European Joint Conferences on Theory and Practice of Software, {ETAPS}
326               2014, Grenoble, France, April 5-13, 2014. Proceedings},
327  pages     = {605--619},
328  year      = {2014},
329  url       = {http://dx.doi.org/10.1007/978-3-642-54862-8_53},
330  doi       = {10.1007/978-3-642-54862-8_53},
331  timestamp = {Sun, 23 Mar 2014 11:19:21 +0100},
332  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tacas/BoenderC14},
333  bibsource = {dblp computer science bibliography, http://dblp.org}
334}
335
336@article{Dave:2003:CVB:966221.966235,
337 author = {Dave, Maulik A.},
338 title = {Compiler Verification: A Bibliography},
339 journal = {SIGSOFT Softw. Eng. Notes},
340 issue_date = {November 2003},
341 volume = {28},
342 number = {6},
343 month = nov,
344 year = {2003},
345 issn = {0163-5948},
346 pages = {2--2},
347 numpages = {1},
348 url = {http://doi.acm.org/10.1145/966221.966235},
349 doi = {10.1145/966221.966235},
350 acmid = {966235},
351 publisher = {ACM},
352 address = {New York, NY, USA},
353} 
354
355@inproceedings{Myreen:2009:EPC:1532828.1532830,
356 author = {Myreen, Magnus O. and Slind, Konrad and Gordon, Michael J.},
357 title = {Extensible Proof-Producing Compilation},
358 booktitle = {Proceedings of the 18th International Conference on Compiler Construction: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009},
359 series = {CC '09},
360 year = {2009},
361 isbn = {978-3-642-00721-7},
362 location = {York, UK},
363 pages = {2--16},
364 numpages = {15},
365 url = {http://dx.doi.org/10.1007/978-3-642-00722-4_2},
366 doi = {10.1007/978-3-642-00722-4_2},
367 acmid = {1532830},
368 publisher = {Springer-Verlag},
369 address = {Berlin, Heidelberg},
370} 
371
372@inproceedings{Li:2008:TST:1792734.1792783,
373 author = {Li, Guodong and Slind, Konrad},
374 title = {Trusted Source Translation of a Total Function Language},
375 booktitle = {Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
376 series = {TACAS'08/ETAPS'08},
377 year = {2008},
378 isbn = {3-540-78799-2, 978-3-540-78799-0},
379 location = {Budapest, Hungary},
380 pages = {471--485},
381 numpages = {15},
382 url = {http://dl.acm.org/citation.cfm?id=1792734.1792783},
383 acmid = {1792783},
384 publisher = {Springer-Verlag},
385 address = {Berlin, Heidelberg},
386} 
387
388@inproceedings{Myreen:2009:VLI:1616077.1616105,
389 author = {Myreen, Magnus O. and Gordon, Michael J.},
390 title = {Verified LISP Implementations on ARM, x86 and PowerPC},
391 booktitle = {Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics},
392 series = {TPHOLs '09},
393 year = {2009},
394 isbn = {978-3-642-03358-2},
395 location = {Munich, Germany},
396 pages = {359--374},
397 numpages = {16},
398 url = {http://dx.doi.org/10.1007/978-3-642-03359-9_25},
399 doi = {10.1007/978-3-642-03359-9_25},
400 acmid = {1616105},
401 publisher = {Springer-Verlag},
402 address = {Berlin, Heidelberg},
403}
404
405@article{Tatlock:2010:BEV:1809028.1806611,
406 author = {Tatlock, Zachary and Lerner, Sorin},
407 title = {Bringing Extensibility to Verified Compilers},
408 journal = {SIGPLAN Not.},
409 issue_date = {June 2010},
410 volume = {45},
411 number = {6},
412 month = jun,
413 year = {2010},
414 issn = {0362-1340},
415 pages = {111--121},
416 numpages = {11},
417 url = {http://doi.acm.org/10.1145/1809028.1806611},
418 doi = {10.1145/1809028.1806611},
419 acmid = {1806611},
420 publisher = {ACM},
421 address = {New York, NY, USA},
422 keywords = {compiler optimization, correctness, extensibility},
423} 
424
425@article{Chlipala:2007:CTC:1273442.1250742,
426 author = {Chlipala, Adam},
427 title = {A Certified Type-preserving Compiler from Lambda Calculus to Assembly Language},
428 journal = {SIGPLAN Not.},
429 issue_date = {June 2007},
430 volume = {42},
431 number = {6},
432 month = jun,
433 year = {2007},
434 issn = {0362-1340},
435 pages = {54--65},
436 numpages = {12},
437 url = {http://doi.acm.org/10.1145/1273442.1250742},
438 doi = {10.1145/1273442.1250742},
439 acmid = {1250742},
440 publisher = {ACM},
441 address = {New York, NY, USA},
442 keywords = {compiler verification, denotational semantics, dependent types, interactive proof assistants},
443} 
444
445@article{Chlipala:2010:VCI:1707801.1706312,
446 author = {Chlipala, Adam},
447 title = {A Verified Compiler for an Impure Functional Language},
448 journal = {SIGPLAN Not.},
449 issue_date = {January 2010},
450 volume = {45},
451 number = {1},
452 month = jan,
453 year = {2010},
454 issn = {0362-1340},
455 pages = {93--106},
456 numpages = {14},
457 url = {http://doi.acm.org/10.1145/1707801.1706312},
458 doi = {10.1145/1707801.1706312},
459 acmid = {1706312},
460 publisher = {ACM},
461 address = {New York, NY, USA},
462 keywords = {compiler verification, interactive proof assistants},
463}
464
465@misc { dwarf,
466  title = {The {DWARF} debugging format standard},
467  url = {http://www.dwarfstd.org/},
468  note = {Accessed March 2017},
469  year = {2017},
470  key = {dwarf}
471}
472
473@inproceedings{DBLP:conf/sefm/BarthePS05,
474  author    = {Gilles Barthe and
475               Mariela Pavlova and
476               Gerardo Schneider},
477  title     = {Precise Analysis of Memory Consumption using Program Logics},
478  booktitle = {Third {IEEE} International Conference on Software Engineering and
479               Formal Methods {(SEFM} 2005), 7-9 September 2005, Koblenz, Germany},
480  pages     = {86--95},
481  year      = {2005},
482  url       = {http://dx.doi.org/10.1109/SEFM.2005.34},
483  doi       = {10.1109/SEFM.2005.34},
484  timestamp = {Fri, 29 May 2015 14:21:25 +0200},
485  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sefm/BarthePS05},
486  bibsource = {dblp computer science bibliography, http://dblp.org}
487}
488
489@Inbook{DalZilio2005,
490author="Dal Zilio, Silvano
491and Gascon, R{\'e}gis",
492editor="Yi, Kwangkeun",
493title="Resource Bound Certification for a Tail-Recursive Virtual Machine",
494bookTitle="Programming Languages and Systems: Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005. Proceedings",
495year="2005",
496publisher="Springer Berlin Heidelberg",
497address="Berlin, Heidelberg",
498pages="247--263",
499isbn="978-3-540-32247-4",
500doi="10.1007/11575467_17",
501url="http://dx.doi.org/10.1007/11575467_17"
502}
503
504
505@Inbook{Chander2005,
506author="Chander, Ajay
507and Espinosa, David
508and Islam, Nayeem
509and Lee, Peter
510and Necula, George",
511editor="Sagiv, Mooly",
512title="Enforcing Resource Bounds via Static Verification of Dynamic Checks",
513bookTitle="Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings",
514year="2005",
515publisher="Springer Berlin Heidelberg",
516address="Berlin, Heidelberg",
517pages="311--325",
518isbn="978-3-540-31987-0",
519doi="10.1007/978-3-540-31987-0_22",
520url="http://dx.doi.org/10.1007/978-3-540-31987-0_22"
521}
522
523
524@Inbook{He2009,
525author="He, Guanhua
526and Qin, Shengchao
527and Luo, Chenguang
528and Chin, Wei-Ngan",
529editor="Liu, Zhiming
530and Ravn, Anders P.",
531title="Memory Usage Verification Using Hip/Sleek",
532bookTitle="Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings",
533year="2009",
534publisher="Springer Berlin Heidelberg",
535address="Berlin, Heidelberg",
536pages="166--181",
537isbn="978-3-642-04761-9",
538doi="10.1007/978-3-642-04761-9_14",
539url="http://dx.doi.org/10.1007/978-3-642-04761-9_14"
540}
541
542
543@inproceedings{Chin:2008:AMR:1375634.1375656,
544 author = {Chin, Wei-Ngan and Nguyen, Huu Hai and Popeea, Corneliu and Qin, Shengchao},
545 title = {Analysing Memory Resource Bounds for Low-level Programs},
546 booktitle = {Proceedings of the 7th International Symposium on Memory Management},
547 series = {ISMM '08},
548 year = {2008},
549 isbn = {978-1-60558-134-7},
550 location = {Tucson, AZ, USA},
551 pages = {151--160},
552 numpages = {10},
553 url = {http://doi.acm.org/10.1145/1375634.1375656},
554 doi = {10.1145/1375634.1375656},
555 acmid = {1375656},
556 publisher = {ACM},
557 address = {New York, NY, USA},
558 keywords = {fixpoint analysis, heap space analysis, low level programs, stack space analysis},
559} 
560
561
562@inproceedings{speed-precise-and-efficient-static-estimation-of-program-computational-complexity-2,
563author = {Gulwani, Sumit and Mehra, Krishna and Chilimbi, Trishul},
564title = {SPEED: Precise and Efficient Static Estimation of Program Computational Complexity},
565booktitle = {Principles of Programming Languages (POPL)},
566year = {2009},
567month = {January},
568abstract = {
569
570This paper describes an inter-procedural technique for computing symbolic bounds on the number of statements a procedure executes in terms of its scalar inputs and user-defined quantitative functions of input data-structures. Such computational complexity bounds for even simple programs are usually disjunctive, non-linear, and involve numerical properties of heaps. We address the challenges of generating these bounds using two novel ideas. We introduce a proof methodology based on multiple counter instrumentation (each counter can be initialized and incremented at potentially multiple program locations) that allows a given linear invariant generation tool to compute linear bounds individually onthese counter variables. The bounds on these counters are then composed together to generate total bounds that are non-linear and disjunctive. We also give an algorithm for automating this proof methodology. Our algorithm generates complexity bounds that are usually precise not only in terms of the computational complexity,but also in terms of the constant factors. Next, we introduce the notion of user-defined quantitative functions that can be associated with abstract data-structures, e.g., length of a list, height of a tree, etc. We show how to compute bounds in terms of these quantitative functions using a linear invariant generation tool that has support for handling uninterpreted functions. We show application of this methodology to commonly used data-structures (namely lists, list of lists, trees, bit-vectors) using examples from Microsoft product code. We observe that a few quantitative functions for each data-structure are usually sufficient to allow generation of symbolic complexity bounds of a variety of loops that iterate over these data-structures, and that it is straightforward to define these quantitative functions. The combination of these techniques enables generation of precise computational complexity bounds for real-world examples (drawn from Microsoft product code and C++ STL library code) for some of which it is non-trivial to even prove termination. Such automatically generated bounds are very useful for early detection of egregious performance problems in large modular codebases that are constantly being changed by multiple developers who make heavy use of code written by others without a good understanding of their implementation complexity.
571
572
573},
574publisher = {Association for Computing Machinery, Inc.},
575url = {https://www.microsoft.com/en-us/research/publication/speed-precise-and-efficient-static-estimation-of-program-computational-complexity-2/},
576address = {},
577pages = {},
578journal = {},
579volume = {},
580chapter = {},
581isbn = {},
582}
583
584@article{DBLP:journals/jot/BrabermanGY06,
585  author    = {V{\'{\i}}ctor A. Braberman and
586               Diego Garbervetsky and
587               Sergio Yovine},
588  title     = {A Static Analysis for Synthesizing Parametric Specifications of Dynamic
589               Memory Consumption},
590  journal   = {Journal of Object Technology},
591  volume    = {5},
592  number    = {5},
593  pages     = {31--58},
594  year      = {2006},
595  url       = {http://dx.doi.org/10.5381/jot.2006.5.5.a2},
596  doi       = {10.5381/jot.2006.5.5.a2},
597  timestamp = {Fri, 19 Nov 2010 11:56:11 +0100},
598  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jot/BrabermanGY06},
599  bibsource = {dblp computer science bibliography, http://dblp.org}
600}
601
602@techreport { symbolic-prediction-2007,
603  author = {V. Braberman and F. Fernandez and D. Garbervetsky and S. Yovine},
604  title = {Symbolic Prediction of Dynamic-Memory Requirements},
605  year = {2007},
606  institute = {VeriMag},
607  number = {TR-2007-11}
608}
609
610@article {DLTC:DLTC280,
611author = {Gödel, Von Kurt},
612title = {\"{U}BER EINE BISHER NOCH NICHT BEN\"UTZTE ERWEITERUNG DES FINITEN STANDPUNKTES},
613journal = {Dialectica},
614volume = {12},
615number = {3-4},
616publisher = {Blackwell Publishing Ltd},
617issn = {1746-8361},
618url = {http://dx.doi.org/10.1111/j.1746-8361.1958.tb01464.x},
619doi = {10.1111/j.1746-8361.1958.tb01464.x},
620pages = {280--287},
621year = {1958},
622}
623
624
625
626@article{DBLP:journals/tocl/AspertiR02,
627  author    = {Andrea Asperti and
628               Luca Roversi},
629  title     = {Intuitionistic Light Affine Logic},
630  journal   = {{ACM} Trans. Comput. Log.},
631  volume    = {3},
632  number    = {1},
633  pages     = {137--175},
634  year      = {2002},
635  url       = {http://doi.acm.org/10.1145/504077.504081},
636  doi       = {10.1145/504077.504081},
637  timestamp = {Fri, 21 Nov 2003 08:34:41 +0100},
638  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tocl/AspertiR02},
639  bibsource = {dblp computer science bibliography, http://dblp.org}
640}
641
642
643@article{GIRARD19871,
644title = "Linear logic",
645journal = "Theoretical Computer Science",
646volume = "50",
647number = "1",
648pages = "1 - 101",
649year = "1987",
650note = "",
651issn = "0304-3975",
652doi = "http://dx.doi.org/10.1016/0304-3975(87)90045-4",
653url = "http://www.sciencedirect.com/science/article/pii/0304397587900454",
654author = "Jean-Yves Girard",
655
656}
657
658@misc { mathematica,
659  title = {Wolfram {Mathematica} website},
660  url = {https://www.wolfram.com/mathematica/},
661  note = {Accessed March 2017},
662  year = {2017},
663  key = {mathematica}
664}
665
666@Article{Albert2011,
667author="Albert, Elvira
668and Arenas, Puri
669and Genaim, Samir
670and Puebla, Germ{\'a}n",
671title="Closed-Form Upper Bounds in Static Cost Analysis",
672journal="Journal of Automated Reasoning",
673year="2011",
674volume="46",
675number="2",
676pages="161--203",
677abstract="The classical approach to automatic cost analysis consists of two phases. Given a program and some measure of cost, the analysis first produces cost relations (CRs), i.e., recursive equations which capture the cost of the program in terms of the size of its input data. Second, CRs are converted into closed-form, i.e., without recurrences. Whereas the first phase has received considerable attention, with a number of cost analyses available for a variety of programming languages, the second phase has been comparatively less studied. This article presents, to our knowledge, the first practical framework for the generation of closed-form upper bounds for CRs which (1) is fully automatic, (2) can handle the distinctive features of CRs, originating from cost analysis of realistic programming languages, (3) is not restricted to simple complexity classes, and (4) produces reasonably accurate solutions. A key idea in our approach is to view CRs as programs, which allows applying semantic-based static analyses and transformations to bound them, namely our method is based on the inference of ranking functions and loop invariants and on the use of partial evaluation.",
678issn="1573-0670",
679doi="10.1007/s10817-010-9174-1",
680url="http://dx.doi.org/10.1007/s10817-010-9174-1"
681}
682
683
684@article{ALBERT200767,
685title = "Experiments in Cost Analysis of Java Bytecode",
686journal = "Electronic Notes in Theoretical Computer Science",
687volume = "190",
688number = "1",
689pages = "67 - 83",
690year = "2007",
691note = "",
692issn = "1571-0661",
693doi = "http://dx.doi.org/10.1016/j.entcs.2007.02.061",
694url = "http://www.sciencedirect.com/science/article/pii/S1571066107005294",
695author = "E. Albert and P. Arenas and S. Genaim and G. Puebla and D. Zanardini",
696keywords = "Cost analysis",
697keywords = "Java bytecode",
698keywords = "cost relations",
699keywords = "recurrence equations",
700keywords = "complexity"
701}
702
703@article{Wang:2014:CVM:2714064.2660201,
704 author = {Wang, Peng and Cuellar, Santiago and Chlipala, Adam},
705 title = {Compiler Verification Meets Cross-language Linking via Data Abstraction},
706 journal = {SIGPLAN Not.},
707 issue_date = {October 2014},
708 volume = {49},
709 number = {10},
710 month = oct,
711 year = {2014},
712 issn = {0362-1340},
713 pages = {675--690},
714 numpages = {16},
715 url = {http://doi.acm.org/10.1145/2714064.2660201},
716 doi = {10.1145/2714064.2660201},
717 acmid = {2660201},
718 publisher = {ACM},
719 address = {New York, NY, USA},
720 keywords = {abstract data types, compiler verification, cross-language linking, program logics},
721} 
722
723@article{KLEIN200427,
724title = "Verified bytecode verification and type-certifying compilation",
725journal = "The Journal of Logic and Algebraic Programming",
726volume = "58",
727number = "1",
728pages = "27 - 60",
729year = "2004",
730note = "",
731issn = "1567-8326",
732doi = "http://dx.doi.org/10.1016/j.jlap.2003.07.004",
733url = "http://www.sciencedirect.com/science/article/pii/S1567832603000754",
734author = "Gerwin Klein and Martin Strecker",
735keywords = "Java",
736keywords = "JVM",
737keywords = "Compiler",
738keywords = "Bytecode verification",
739keywords = "Theorem proving"
740}
741
742@Inbook{Strecker2002,
743author="Strecker, Martin",
744editor="Voronkov, Andrei",
745title="Formal Verification of a Java Compiler in Isabelle",
746bookTitle="Automated Deduction---CADE-18: 18th International Conference on Automated Deduction Copenhagen, Denmark, July 27--30, 2002 Proceedings",
747year="2002",
748publisher="Springer Berlin Heidelberg",
749address="Berlin, Heidelberg",
750pages="63--77",
751isbn="978-3-540-45620-9",
752doi="10.1007/3-540-45620-1_5",
753url="http://dx.doi.org/10.1007/3-540-45620-1_5"
754}
755
756@article{Kumar:2014:CVI:2578855.2535841,
757 author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott},
758 title = {CakeML: A Verified Implementation of ML},
759 journal = {SIGPLAN Not.},
760 issue_date = {January 2014},
761 volume = {49},
762 number = {1},
763 month = jan,
764 year = {2014},
765 issn = {0362-1340},
766 pages = {179--191},
767 numpages = {13},
768 url = {http://doi.acm.org/10.1145/2578855.2535841},
769 doi = {10.1145/2578855.2535841},
770 acmid = {2535841},
771 publisher = {ACM},
772 address = {New York, NY, USA},
773 keywords = {ML, compiler bootstrapping, compiler verification, machine code verification, read-eval-print loop, verified garbage collection., verified parsing, verified type checking},
774} 
775
776@inproceedings{Rideau-Leroy-regalloc,
777  author = {Silvain Rideau and Xavier Leroy},
778  title = {Validating register allocation and spilling},
779  booktitle = {Compiler Construction (CC 2010)},
780  year = 2010,
781  publisher = {Springer},
782  series = {Lecture Notes in Computer Science},
783  volume = 6011,
784  pages = {224-243},
785  xtopic = {compcert},
786  url = {http://gallium.inria.fr/~xleroy/publi/validation-regalloc.pdf},
787  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-11970-5_13},
788  abstract = {Following the translation validation approach to high-assurance
789compilation, we describe a new algorithm for validating {\em a
790posteriori} the results of a run of register allocation.  The
791algorithm is based on backward dataflow inference of
792equations between variables, registers and stack locations, and can
793cope with sophisticated forms of spilling and live range splitting, as
794well as many forms of architectural irregularities such as overlapping
795registers.  The soundness of the algorithm was mechanically proved
796using the Coq proof assistant.}
797}
798
799@inproceedings{Blazy-Robillard-splitting,
800  author = {Sandrine Blazy and Benoît Robillard},
801  title = {Live-range Unsplitting for Faster Optimal Coalescing},
802  booktitle = {Proceedings of the ACM SIGPLAN/SIGBED 2009
803                         conference on Languages,
804                         Compilers, and Tools for Embedded Systems
805                         (LCTES 2009)},
806  pages = {70--79},
807  publisher = {ACM Press},
808  year = 2009,
809  url = {http://www.ensiie.fr/~blazy/LCTES09.pdf},
810  urlpublisher = {http://doi.acm.org/10.1145/1542452.1542462},
811  hal = {http://hal.inria.fr/inria-00387749/},
812  pubkind = {conf-int-mono}
813}
814
815@article{Regehr:2005:ESO:1113830.1113833,
816 author = {Regehr, John and Reid, Alastair and Webb, Kirk},
817 title = {Eliminating Stack Overflow by Abstract Interpretation},
818 journal = {ACM Trans. Embed. Comput. Syst.},
819 issue_date = {November 2005},
820 volume = {4},
821 number = {4},
822 month = nov,
823 year = {2005},
824 issn = {1539-9087},
825 pages = {751--778},
826 numpages = {28},
827 url = {http://doi.acm.org/10.1145/1113830.1113833},
828 doi = {10.1145/1113830.1113833},
829 acmid = {1113833},
830 publisher = {ACM},
831 address = {New York, NY, USA},
832 keywords = {Microcontroller, abstract interpretation, call stack, context sensitive, dataflow analysis, interrupt-driven, sensor network},
833}
834
835@inproceedings{DBLP:conf/esop/HofmannJ06,
836  author    = {Martin Hofmann and
837               Steffen Jost},
838  title     = {Type-Based Amortised Heap-Space Analysis},
839  booktitle = {Programming Languages and Systems, 15th European Symposium on Programming,
840               {ESOP} 2006, Held as Part of the Joint European Conferences on Theory
841               and Practice of Software, {ETAPS} 2006, Vienna, Austria, March 27-28,
842               2006, Proceedings},
843  pages     = {22--37},
844  year      = {2006},
845  url       = {http://dx.doi.org/10.1007/11693024_3},
846  doi       = {10.1007/11693024_3},
847  timestamp = {Thu, 28 May 2015 17:23:23 +0200},
848  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/esop/HofmannJ06},
849  bibsource = {dblp computer science bibliography, http://dblp.org}
850}
851
852@phdthesis{bac-thesis08,
853  title = {Type-based amortized stack memory prediction},
854  author = {Brian Campbell},
855  school = {University of Edinburgh},
856  year = 2008
857}
858
859@inproceedings{bac-giveback08,
860  title = {Prediction of linear memory usage for first-order functional programs},
861  author = {Brian Campbell},
862  booktitle = {Trends in Functional Programming},
863  editor = {Peter Achten and Pieter Koopman and Moraz\'an, Marco T.},
864  volume = 9,
865  year = 2009,
866  pages = {1--16},
867  publisher = {Intellect},
868  isbn = {978-1-84150-277-9}
869}
870
871@Inbook{DalLago2012,
872author="Dal Lago, Ugo",
873editor="Bezhanishvili, Nick
874and Goranko, Valentin",
875title="A Short Introduction to Implicit Computational Complexity",
876bookTitle="Lectures on Logic and Computation: ESSLLI 2010 Copenhagen, Denmark, August 2010, ESSLLI 2011, Ljubljana, Slovenia, August 2011, Selected Lecture Notes",
877year="2012",
878publisher="Springer Berlin Heidelberg",
879address="Berlin, Heidelberg",
880pages="89--109",
881isbn="978-3-642-31485-8",
882doi="10.1007/978-3-642-31485-8_3",
883url="http://dx.doi.org/10.1007/978-3-642-31485-8_3"
884}
885
886@misc { clang,
887  url = {https://clang.llvm.org/},
888  title = {The {clang} {C} language frontend for {LLVM}},
889  note = {Accessed March 2017},
890  year = {2017},
891  key = {clang}
892}
893
894@misc { gcc,
895  url = {https://gcc.gnu.org/},
896  title = {The {GNU} compiler collection},
897  note = {Accessed March 2017},
898  year = {2017},
899  key = {gcc}
900}
901
902@misc { icc,
903  url = {https://software.intel.com/en-us/c-compilers},
904  title = {The {Intel} {C} and {C++} compiler},
905  note = {Accessed March 2017},
906  year = {2017},
907  key = {icc}
908}
909
910@inproceedings{bac-esop09,
911  title = {Amortised Memory Analysis using the Depth of Data Structures},
912  author = {Brian Campbell},
913  booktitle = {Programming Languages and Systems: 18th European Symposium on Programming (ESOP 2009)},
914  pages = {190--204},
915  year = 2009,
916  editor = {Giuseppe Castagna},
917  volume = 5502,
918  series = {Lecture Notes in Computer Science},
919  publisher = {Springer-Verlag},
920  doi = {10.1007/978-3-642-00590-9_14}
921}
922
923@Inbook{Chalin2006,
924author="Chalin, Patrice
925and Kiniry, Joseph R.
926and Leavens, Gary T.
927and Poll, Erik",
928editor="de Boer, Frank S.
929and Bonsangue, Marcello M.
930and Graf, Susanne
931and de Roever, Willem-Paul",
932title="Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2",
933bookTitle="Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures",
934year="2006",
935publisher="Springer Berlin Heidelberg",
936address="Berlin, Heidelberg",
937pages="342--363",
938isbn="978-3-540-36750-5",
939doi="10.1007/11804192_16",
940url="http://dx.doi.org/10.1007/11804192_16"
941}
942
943
944@book{KeYBook2016,
945title = {Deductive Software Verification - The KeY Book - From Theory to Practice},
946editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"{a}}hnle and Peter H. Schmitt and Mattias Ulbrich},
947url = {http://dx.doi.org/10.1007/978-3-319-49812-6},
948doi = {10.1007/978-3-319-49812-6},
949isbn = {978-3-319-49811-9},
950year = {2016},
951date = {2016-12-16},
952volume = {10001},
953publisher = {Springer},
954series = {Lecture Notes in Computer Science},
955keywords = {},
956pubstate = {published},
957tppubtype = {book}
958}
959
960
961
962@Inbook{Montenegro2010a,
963author="Montenegro, Manuel
964and Pe{\~{n}}a, Ricardo
965and Segura, Clara",
966editor="van Eekelen, Marko
967and Shkaravska, Olha",
968title="A Space Consumption Analysis by Abstract Interpretation",
969bookTitle="Foundational and Practical Aspects of Resource Analysis: First International Workshop, FOPARA 2009, Eindhoven, The Netherlands, November 6, 2009, Revised Selected Papers",
970year="2010",
971publisher="Springer Berlin Heidelberg",
972address="Berlin, Heidelberg",
973pages="34--50",
974isbn="978-3-642-15331-0",
975doi="10.1007/978-3-642-15331-0_3",
976url="http://dx.doi.org/10.1007/978-3-642-15331-0_3"
977}
978
979
980@Inbook{Montenegro2010,
981author="Montenegro, Manuel
982and Pe{\~{n}}a, Ricardo
983and Segura, Clara",
984editor="Escobar, Santiago",
985title="A Simple Region Inference Algorithm for a First-Order Functional Language",
986bookTitle="Functional and Constraint Logic Programming: 18th International Workshop, WFLP 2009, Brasilia, Brazil, June 28, 2009, Revised Selected Papers",
987year="2010",
988publisher="Springer Berlin Heidelberg",
989address="Berlin, Heidelberg",
990pages="145--161",
991isbn="978-3-642-11999-6",
992doi="10.1007/978-3-642-11999-6_10",
993url="http://dx.doi.org/10.1007/978-3-642-11999-6_10"
994}
995
996
997@Inbook{deDios2011,
998author="de Dios, Javier
999and Pe{\~{n}}a, Ricardo",
1000editor="Butler, Michael
1001and Schulte, Wolfram",
1002title="Certification of Safe Polynomial Memory Bounds",
1003bookTitle="FM 2011: Formal Methods: 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings",
1004year="2011",
1005publisher="Springer Berlin Heidelberg",
1006address="Berlin, Heidelberg",
1007pages="184--199",
1008isbn="978-3-642-21437-0",
1009doi="10.1007/978-3-642-21437-0_16",
1010url="http://dx.doi.org/10.1007/978-3-642-21437-0_16"
1011}
1012
1013
1014@Inbook{Albert2012,
1015author="Albert, Elvira
1016and Bubel, Richard
1017and Genaim, Samir
1018and H{\"a}hnle, Reiner
1019and Rom{\'a}n-D{\'i}ez, Guillermo",
1020editor="de Lara, Juan
1021and Zisman, Andrea",
1022title="Verified Resource Guarantees for Heap Manipulating Programs",
1023bookTitle="Fundamental Approaches to Software Engineering: 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings",
1024year="2012",
1025publisher="Springer Berlin Heidelberg",
1026address="Berlin, Heidelberg",
1027pages="130--145",
1028isbn="978-3-642-28872-2",
1029doi="10.1007/978-3-642-28872-2_10",
1030url="http://dx.doi.org/10.1007/978-3-642-28872-2_10"
1031}
1032
1033
1034@Inbook{Nipkow2015,
1035author="Nipkow, Tobias",
1036editor="Urban, Christian
1037and Zhang, Xingyuan",
1038title="Amortized Complexity Verified",
1039bookTitle="Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings",
1040year="2015",
1041publisher="Springer International Publishing",
1042address="Cham",
1043pages="310--324",
1044isbn="978-3-319-22102-1",
1045doi="10.1007/978-3-319-22102-1_21",
1046url="http://dx.doi.org/10.1007/978-3-319-22102-1_21"
1047}
1048
1049
1050@article{Hoffmann:2012:MAR:2362389.2362393,
1051 author = {Hoffmann, Jan and Aehlig, Klaus and Hofmann, Martin},
1052 title = {Multivariate Amortized Resource Analysis},
1053 journal = {ACM Trans. Program. Lang. Syst.},
1054 issue_date = {October 2012},
1055 volume = {34},
1056 number = {3},
1057 month = nov,
1058 year = {2012},
1059 issn = {0164-0925},
1060 pages = {14:1--14:62},
1061 articleno = {14},
1062 numpages = {62},
1063 url = {http://doi.acm.org/10.1145/2362389.2362393},
1064 doi = {10.1145/2362389.2362393},
1065 acmid = {2362393},
1066 publisher = {ACM},
1067 address = {New York, NY, USA},
1068 keywords = {Amortized analysis, functional programming, quantitative analysis, resource consumption, static analysis},
1069} 
1070
1071
1072
1073@Inbook{Chargueraud2015,
1074author="Chargu{\'e}raud, Arthur
1075and Pottier, Fran{\c{c}}ois",
1076editor="Urban, Christian
1077and Zhang, Xingyuan",
1078title="Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation",
1079bookTitle="Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings",
1080year="2015",
1081publisher="Springer International Publishing",
1082address="Cham",
1083pages="137--153",
1084isbn="978-3-319-22102-1",
1085doi="10.1007/978-3-319-22102-1_9",
1086url="http://dx.doi.org/10.1007/978-3-319-22102-1_9"
1087}
1088
1089
1090@Inbook{Teller2002,
1091author="Teller, David
1092and Zimmer, Pascal
1093and Hirschkoff, Daniel",
1094editor="Brim, Lubo{\v{s}}
1095and K{\v{r}}et{\'i}nsk{\'y}, Mojm{\'i}r
1096and Ku{\v{c}}era, Anton{\'i}n
1097and Jan{\v{c}}ar, Petr",
1098title="Using Ambients to Control Resources*                  ",
1099bookTitle="CONCUR 2002 --- Concurrency Theory: 13th International Conference Brno, Czech Republic, August 20--23, 2002 Proceedings",
1100year="2002",
1101publisher="Springer Berlin Heidelberg",
1102address="Berlin, Heidelberg",
1103pages="288--303",
1104isbn="978-3-540-45694-0",
1105doi="10.1007/3-540-45694-5_20",
1106url="http://dx.doi.org/10.1007/3-540-45694-5_20"
1107}
1108
1109
1110@article{DBLP:journals/jfp/0002S15,
1111  author    = {Jan Hoffmann and
1112               Zhong Shao},
1113  title     = {Type-based amortized resource analysis with integers and arrays},
1114  journal   = {J. Funct. Program.},
1115  volume    = {25},
1116  year      = {2015},
1117  url       = {http://dx.doi.org/10.1017/S0956796815000192},
1118  doi       = {10.1017/S0956796815000192},
1119  timestamp = {Tue, 26 Jan 2016 16:08:20 +0100},
1120  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jfp/0002S15},
1121  bibsource = {dblp computer science bibliography, http://dblp.org}
1122}
1123
1124@Inbook{Barbanera2003,
1125author="Barbanera, Franco
1126and Bugliesi, Michele
1127and Dezani-Ciancaglini, Mariangiola
1128and Sassone, Vladimiro",
1129editor="Saraswat, Vijay A.",
1130title="A Calculus of Bounded Capacities",
1131bookTitle="Advances in Computing Science -- ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation: 8th Asian Computing Science Conference, Mumbai, India, December 10-12, 2003. Proceedings",
1132year="2003",
1133publisher="Springer Berlin Heidelberg",
1134address="Berlin, Heidelberg",
1135pages="205--223",
1136isbn="978-3-540-40965-6",
1137doi="10.1007/978-3-540-40965-6_14",
1138url="http://dx.doi.org/10.1007/978-3-540-40965-6_14"
1139}
1140
1141@article{Danielsson:2008:LST:1328897.1328457,
1142 author = {Danielsson, Nils Anders},
1143 title = {Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures},
1144 journal = {SIGPLAN Not.},
1145 issue_date = {January 2008},
1146 volume = {43},
1147 number = {1},
1148 month = jan,
1149 year = {2008},
1150 issn = {0362-1340},
1151 pages = {133--144},
1152 numpages = {12},
1153 url = {http://doi.acm.org/10.1145/1328897.1328457},
1154 doi = {10.1145/1328897.1328457},
1155 acmid = {1328457},
1156 publisher = {ACM},
1157 address = {New York, NY, USA},
1158 keywords = {amortised time complexity, dependent types, lazy evaluation, purely functional data structures},
1159} 
1160
1161
1162@inproceedings{Crary:2000:RBC:325694.325716,
1163 author = {Crary, Karl and Weirich, Stephnie},
1164 title = {Resource Bound Certification},
1165 booktitle = {Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
1166 series = {POPL '00},
1167 year = {2000},
1168 isbn = {1-58113-125-9},
1169 location = {Boston, MA, USA},
1170 pages = {184--198},
1171 numpages = {15},
1172 url = {http://doi.acm.org/10.1145/325694.325716},
1173 doi = {10.1145/325694.325716},
1174 acmid = {325716},
1175 publisher = {ACM},
1176 address = {New York, NY, USA},
1177} 
1178
1179@Inbook{McCarthy2016,
1180author="McCarthy, Jay
1181and Fetscher, Burke
1182and New, Max
1183and Feltey, Daniel
1184and Findler, Robert Bruce",
1185editor="Kiselyov, Oleg
1186and King, Andy",
1187title="A Coq Library for Internal Verification of Running-Times",
1188bookTitle="Functional and Logic Programming: 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings",
1189year="2016",
1190publisher="Springer International Publishing",
1191address="Cham",
1192pages="144--162",
1193isbn="978-3-319-29604-3",
1194doi="10.1007/978-3-319-29604-3_10",
1195url="http://dx.doi.org/10.1007/978-3-319-29604-3_10"
1196}
1197
1198@inproceedings { chan-ngo-verifying-2017,
1199  title = {Verifying and Synthesizing Constant-Resource Implementations with Types},
1200  author = {Van Chan Ngo and Mario Dehesa-Azuara and Matthew Fredrikson and Jan Hoffmann},
1201  booktitle = {Proceedings of the {IEEE} Symposium on Security and Privacy},
1202  year = {2017},
1203  note = {to appear}
1204}
1205
1206@Inbook{Brady2006,
1207author="Brady, Edwin
1208and Hammond, Kevin",
1209editor="Butterfield, Andrew
1210and Grelck, Clemens
1211and Huch, Frank",
1212title="A Dependently Typed Framework for Static Analysis of Program Execution Costs",
1213bookTitle="Implementation and Application of Functional Languages: 17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers",
1214year="2006",
1215publisher="Springer Berlin Heidelberg",
1216address="Berlin, Heidelberg",
1217pages="74--90",
1218isbn="978-3-540-69175-4",
1219doi="10.1007/11964681_5",
1220url="http://dx.doi.org/10.1007/11964681_5"
1221}
1222
1223
1224@inproceedings{Danner:2013:SCA:2428116.2428123,
1225 author = {Danner, Norman and Paykin, Jennifer and Royer, James S.},
1226 title = {A Static Cost Analysis for a Higher-order Language},
1227 booktitle = {Proceedings of the 7th Workshop on Programming Languages Meets Program Verification},
1228 series = {PLPV '13},
1229 year = {2013},
1230 isbn = {978-1-4503-1860-0},
1231 location = {Rome, Italy},
1232 pages = {25--34},
1233 numpages = {10},
1234 url = {http://doi.acm.org/10.1145/2428116.2428123},
1235 doi = {10.1145/2428116.2428123},
1236 acmid = {2428123},
1237 publisher = {ACM},
1238 address = {New York, NY, USA},
1239 keywords = {automated theorem proving, certified bounds, higher-order complexity},
1240} 
1241
1242
1243@inproceedings{Reynolds:2002:SLL:645683.664578,
1244 author = {Reynolds, John C.},
1245 title = {Separation Logic: A Logic for Shared Mutable Data Structures},
1246 booktitle = {Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science},
1247 series = {LICS '02},
1248 year = {2002},
1249 isbn = {0-7695-1483-9},
1250 pages = {55--74},
1251 numpages = {20},
1252 url = {http://dl.acm.org/citation.cfm?id=645683.664578},
1253 acmid = {664578},
1254 publisher = {IEEE Computer Society},
1255 address = {Washington, DC, USA},
1256} 
1257
1258@article{ASPINALL2007411,
1259title = "A program logic for resources",
1260journal = "Theoretical Computer Science",
1261volume = "389",
1262number = "3",
1263pages = "411 - 445",
1264year = "2007",
1265note = "",
1266issn = "0304-3975",
1267doi = "http://dx.doi.org/10.1016/j.tcs.2007.09.003",
1268url = "http://www.sciencedirect.com/science/article/pii/S0304397507006627",
1269author = "David Aspinall and Lennart Beringer and Martin Hofmann and Hans-Wolfgang Loidl and Alberto Momigliano",
1270}
1271
1272@inproceedings{HoffHof10,
1273  author    = {Jan Hoffmann and
1274               Martin Hofmann},
1275  title     = {{Amortized Resource Analysis with Polynomial Potential - A
1276             Static Inference of Polynomial Bounds for Functional Programs}},
1277  booktitle = {{In Proceedings of the 19th European Symposium on Programming (ESOP'10)}},
1278  pages     = {287-306},
1279  publisher = {Springer},
1280  series    = {Lecture Notes in Computer Science},
1281  volume    = {6012},
1282  year      = {2010}
1283}
1284
1285
1286@article{HAH12Toplas,
1287 author = {Jan Hoffmann and Klaus Aehlig and Martin Hofmann},
1288 title = {{Multivariate Amortized Resource Analysis}},
1289 journal = {ACM Trans. Program. Lang. Syst.},
1290 issue_date = {October 2012},
1291 volume = {34},
1292 number = {3},
1293 month = nov,
1294 year = {2012},
1295 issn = {0164-0925},
1296 pages = {14:1--14:62},
1297 articleno = {14},
1298 numpages = {62},
1299 url = {http://doi.acm.org/10.1145/2362389.2362393},
1300 doi = {10.1145/2362389.2362393},
1301 acmid = {2362393},
1302 publisher = {ACM},
1303 address = {New York, NY, USA},
1304 keywords = {Amortized analysis, functional programming, quantitative analysis, resource consumption, static analysis},
1305} 
1306
1307
1308@misc { bound-T,
1309  title = {bound-T {WCET} analysis tool, user guide},
1310  url = {http://www.bound-t.com/manuals/user-guide.pdf},
1311  author = {Tidorum Ltd.},
1312  note = {Accessed March 2017},
1313  year = {2017},
1314  key = {bound-T user guide}
1315}
1316
1317@misc { otawa,
1318  title = {{OTAWA} {WCET} analysis tool, user guide},
1319  url = {http://www.tracesgroup.net/otawa//doc/manuals/manual/manual.html},
1320  author = {{TRACES team}, {IRIT labs}, {University of Toulouse}},
1321  note = {Accessed March 2017},
1322  year = {2017},
1323  key = {otawa user guide}
1324}
1325
1326@misc { heptane,
1327  title = {Heptane {WCET} analysis tool},
1328  url = {https://team.inria.fr/pacap/software/heptane/},
1329  author = {{Inria} / {IRISA} project-team {PACAP}},
1330  note = {Accessed March 2017},
1331  year = {2017},
1332  key = {Heptane}
1333}
1334
1335@Inbook{Lisper2014,
1336author="Lisper, Bj{\"o}rn",
1337editor="Margaria, Tiziana
1338and Steffen, Bernhard",
1339title="SWEET -- A Tool for WCET Flow Analysis (Extended Abstract)",
1340bookTitle="Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications: 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part II",
1341year="2014",
1342publisher="Springer Berlin Heidelberg",
1343address="Berlin, Heidelberg",
1344pages="482--485",
1345isbn="978-3-662-45231-8",
1346doi="10.1007/978-3-662-45231-8_38",
1347url="http://dx.doi.org/10.1007/978-3-662-45231-8_38"
1348}
1349
1350
1351@inproceedings{Cousot1977,
1352 author = {Cousot, Patrick and Cousot, Radhia},
1353 title = {Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints},
1354 booktitle = {Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages},
1355 series = {POPL '77},
1356 year = {1977},
1357 location = {Los Angeles, California},
1358 pages = {238--252},
1359 numpages = {15},
1360 url = {http://doi.acm.org/10.1145/512950.512973},
1361 doi = {10.1145/512950.512973},
1362 acmid = {512973},
1363 publisher = {ACM},
1364 address = {New York, NY, USA},
1365} 
1366
1367
1368
1369@inproceedings{BoneAFerdCHH2007:IFL,
1370  volume = {4449},
1371  pdf = {http://www-fp.cs.st-andrews.ac.uk/embounded/pubs/papers/ifl06.pdf},
1372  author = {Armelle Bonenfant and Christian Ferdinand and Kevin Hammond and Reinhold
1373    Heckmann},
1374  series = {Lecture Notes in Computer Science},
1375  booktitle = {Proc. Implementation of Functional Languages (IFL 2006)},
1376  title = {Worst-Case Execution Times for a Purely Functional Language},
1377  publisher = {Springer},
1378  year = {2007},
1379  bibsource = {http://www-fp.cs.st-andrews.ac.uk/hume/papers/bib.shtml?2007}
1380}
1381
1382@inproceedings{DBLP:conf/wcet/MaronezeBPP14,
1383  author    = {Andr{\'{e}} Oliveira Maroneze and
1384               Sandrine Blazy and
1385               David Pichardie and
1386               Isabelle Puaut},
1387  title     = {A Formally Verified {WCET} Estimation Tool},
1388  booktitle = {14th International Workshop on Worst-Case Execution Time Analysis,
1389               {WCET} 2014, July 8, 2014, Ulm, Germany},
1390  pages     = {11--20},
1391  year      = {2014},
1392  url       = {http://dx.doi.org/10.4230/OASIcs.WCET.2014.11},
1393  doi       = {10.4230/OASIcs.WCET.2014.11},
1394  timestamp = {Thu, 30 Jun 2016 12:29:27 +0200},
1395  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/wcet/MaronezeBPP14},
1396  bibsource = {dblp computer science bibliography, http://dblp.org}
1397}
1398
1399@inproceedings{BoneAChenZHMWW2007:ACM,
1400  location = {Seoul, Korea},
1401  pdf = {http://www-fp.cs.st-andrews.ac.uk/embounded/pubs/papers/sac2007.pdf},
1402  author = {Armelle Bonenfant and Zezhi Chen and Kevin Hammond and Greg Michaelson and
1403    Andy Wallace and Iain Wallace},
1404  note = {To appear.},
1405  keywords = {hume,embounded},
1406  booktitle = {ACM Symposium on Applied Computing (SAC '07), Seoul, Korea, March 11-15},
1407  url = {http://www.acm.org/conferences/sac/sac2007/},
1408  title = {Towards Resource-Certified Software: A Formal Cost Model for Time and its
1409    Application to an Image-Processing Example},
1410  year = {2007},
1411  bibsource = {http://www-fp.cs.st-andrews.ac.uk/hume/papers/bib.shtml?2007}
1412}
1413
1414
1415@article{cerco,
1416  INIauthor    = {R. Amadio and A. Asperti and N. Ayache and
1417                  B. Campbell and D. P. Mulligan and R. Pollack and
1418                  Y. R{\'e}gis-Gianas and C. Sacerdoti Coen and I.
1419                  Stark},
1420  author    = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
1421                  Brian Campbell and Dominic P. Mulligan and Randy Pollack and
1422                  Yann R{\'e}gis-Gianas and Claudio Sacerdoti Coen and Ian
1423                  Stark},
1424  title     = {Certified Complexity},
1425  journal   = {Procedia Computer Science},
1426  volume    = 7,
1427  year      = 2011,
1428  pages     = {175--177},
1429  doi       = {10.1016/j.procs.2011.09.054},
1430  note      = {Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11)}
1431}
1432
1433@incollection{labelling,
1434year={2012},
1435isbn={978-3-642-32468-0},
1436booktitle={Formal Methods for Industrial Critical Systems},
1437volume={7437},
1438series={LNCS},
1439doi={10.1007/978-3-642-32469-7_3},
1440title={Certifying and Reasoning on Cost Annotations in {C} Programs},
1441url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
1442author={Ayache, Nicolas and Amadio, Roberto and R\'egis-Gianas, Yann},
1443pages={32--46},
1444publisher={Springer Berlin Heidelberg}
1445}
1446
1447@incollection{labelling2,
1448year={2012},
1449booktitle={Foundational and Practical Aspects of Resource Analysis},
1450volume={7177},
1451series={LNCS},
1452doi={10.1007/978-3-642-32495-6_5},
1453title={Certifying and Reasoning on Cost Annotations of Functional Programs},
1454author={Amadio, Roberto and R\'egis-Gianas, Yann},
1455pages={72--89},
1456note={Extended version to appear in Higher Order and Symbolic Computation},
1457publisher={Springer Berlin Heidelberg}
1458}
1459
1460@article{compcert,
1461  author = {Xavier Leroy},
1462  title = {Formal verification of a realistic compiler},
1463  journal = {Communications of the ACM},
1464  year = 2009,
1465  volume = 52,
1466  number = 7,
1467  pages = {107--115},
1468  urlthatwewillskip = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
1469  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
1470  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
1471  pubkind = {journal-int-mono},
1472  abstract = {This paper reports on the development and formal verification (proof
1473of semantic preservation) of CompCert, a compiler from Clight (a
1474large subset of the C programming language) to PowerPC assembly code,
1475using the Coq proof assistant both for programming the compiler and
1476for proving its correctness.  Such a verified compiler is useful in
1477the context of critical software and its formal verification: the
1478verification of the compiler guarantees that the safety properties
1479proved on the source code hold for the executable compiled code as
1480well.}
1481}
1482
1483@Manual{framac,
1484title = {Frama-{C} user manual},
1485author = {L. Correnson and P. Cuoq and F. Kirchner and V. Prevosto and A. Puccetti and J. Signoles and
1486B. Yakobowski},
1487organization = {CEA-LIST, Software Safety Laboratory, Saclay, F-91191},
1488note = {\url{http://frama-c.com/}}
1489}
1490
1491@inproceedings{paolo,
1492 author = {Paolo Tranquilli},
1493 title = {Indexed Labels for Loop Iteration Dependent Costs},
1494 booktitle = {QAPL},
1495 series = {EPTCS},
1496 volume = {117},
1497 doi = {10.4204/EPTCS.117.2},
1498 year = {2013},
1499 pages = {19--23}
1500}
1501
1502@INPROCEEDINGS{separation,
1503    author = {John C. Reynolds},
1504    title = {Intuitionistic Reasoning about Shared Mutable Data Structure},
1505    booktitle = {Millennial Perspectives in Computer Science},
1506    year = {2000},
1507    pages = {303--321},
1508    publisher = {Palgrave}
1509}
1510
1511@inproceedings{lustre,
1512  author    = {Paul Caspi and
1513               Daniel Pilaud and
1514               Nicolas Halbwachs and
1515               John Plaice},
1516  title     = {Lustre: A Declarative Language for Programming Synchronous
1517               Systems},
1518  booktitle = {POPL},
1519  year      = {1987},
1520  pages     = {178-188},
1521  ee        = {http://doi.acm.org/10.1145/41625.41641},
1522  bibsource = {DBLP, http://dblp.uni-trier.de}
1523}
1524@proceedings{DBLP:conf/popl/1987,
1525  title     = {Conference Record of the Fourteenth Annual ACM Symposium
1526               on Principles of Programming Languages, Munich, Germany,
1527               January 21-23, 1987},
1528  booktitle = {POPL},
1529  publisher = {ACM Press},
1530  year      = {1987},
1531  isbn      = {0-89791-215-2},
1532  ee        = {http://dl.acm.org/citation.cfm?id=41625},
1533  bibsource = {DBLP, http://dblp.uni-trier.de}
1534}
1535 
1536@inproceedings{correctness,
1537  author    = {Mulligan, Dominic P.  and
1538               Sacerdoti Coen, Claudio},
1539  title     = {On the Correctness of an Optimising Assembler for the {Intel
1540               MCS-51} Microprocessor},
1541  booktitle = {CPP},
1542  year      = {2012},
1543  pages     = {43--59},
1544  doi       = {10.1007/978-3-642-35308-6_7}
1545}
1546@proceedings{DBLP:conf/cpp/2012,
1547  editor    = {Chris Hawblitzel and
1548               Dale Miller},
1549  title     = {Certified Programs and Proofs - Second International Conference,
1550               CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
1551  booktitle = {CPP},
1552  publisher = {Springer},
1553  series    = {LNCS},
1554  volume    = {7679},
1555  year      = {2012},
1556  isbn      = {978-3-642-35307-9},
1557  ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6},
1558  bibsource = {DBLP, http://dblp.uni-trier.de}
1559}
1560
1561@article{proartis,
1562    title = {PROARTIS: Probabilistically Analysable Real-Time Systems},
1563    journal = {Transactions on Embedded Computing Systems},
1564    year = {2012},
1565    publisher = {ACM},
1566    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}
1567}
1568
1569@inproceedings{embounded,
1570  author    = {Kevin Hammond and
1571               Roy Dyckhoff and
1572               Christian Ferdinand and
1573               Reinhold Heckmann and
1574               Martin Hofmann and
1575               Steffen Jost and
1576               Hans-Wolfgang Loidl and
1577               Greg Michaelson and
1578               Robert F. Pointon and
1579               Norman Scaife and
1580               Jocelyn S{\'e}rot and
1581               Andy Wallace},
1582  title     = {{The {EmBounded} Project (Project Start Paper)}},
1583  booktitle = {TFP},
1584  year      = {2005},
1585  pages     = {195--210}
1586}
1587
1588@proceedings{TFP2005,
1589  title     = {Revised Selected Papers from the Sixth Symposium on Trends
1590               in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
1591               September 2005},
1592  booktitle = {Trends in Functional Programming},
1593  series    = {Trends in Functional Programming},
1594  volume    = {6},
1595  year      = {2007},
1596  isbn      = {978-1-84150-176-5},
1597}
1598
1599@misc
1600{ acsl,
1601  title = {{ACSL}: the {ANSI}/{ISO} {C} specification language, reference manual},
1602  url   = {https://frama-c.com/download/acsl_1.4.pdf},
1603  note  = {Accessed March 2017},
1604  year  = {2017},
1605  key   = {acsl-the}
1606}
1607
1608@inproceedings{DBLP:conf/cav/BarrettT07,
1609  author    = {Clark Barrett and
1610               Cesare Tinelli},
1611  title     = {{CVC3}},
1612  booktitle = {Computer Aided Verification, 19th International Conference, {CAV}
1613               2007, Berlin, Germany, July 3-7, 2007, Proceedings},
1614  pages     = {298--302},
1615  year      = {2007},
1616  url       = {http://dx.doi.org/10.1007/978-3-540-73368-3_34},
1617  doi       = {10.1007/978-3-540-73368-3_34},
1618  timestamp = {Mon, 03 Sep 2007 13:24:22 +0200},
1619  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/BarrettT07},
1620  bibsource = {dblp computer science bibliography, http://dblp.org}
1621}
1622
1623
1624@article{DBLP:journals/corr/abs-1202-4905,
1625  author    = {Andrea Asperti and
1626               Wilmer Ricciotti and
1627               Claudio Sacerdoti Coen and
1628               Enrico Tassi},
1629  title     = {A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive
1630               Constructions},
1631  journal   = {Logical Methods in Computer Science},
1632  volume    = {8},
1633  number    = {1},
1634  year      = {2012},
1635  url       = {http://dx.doi.org/10.2168/LMCS-8(1:18)2012},
1636  doi       = {10.2168/LMCS-8(1:18)2012},
1637  timestamp = {Mon, 15 Oct 2012 13:17:50 +0200},
1638  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1202-4905},
1639  bibsource = {dblp computer science bibliography, http://dblp.org}
1640}
1641
1642
1643@inproceedings{matita,
1644  author    = {Andrea Asperti and
1645               Wilmer Ricciotti and
1646               Claudio Sacerdoti Coen and
1647               Enrico Tassi},
1648  title     = {The {Matita} Interactive Theorem Prover},
1649  booktitle = {CADE},
1650  year      = {2011},
1651  pages     = {64-69},
1652  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6_7},
1653  bibsource = {DBLP, http://dblp.uni-trier.de}
1654}
1655@proceedings{DBLP:conf/cade/2011,
1656  title     = {Automated Deduction - CADE-23 - 23rd International Conference
1657               on Automated Deduction, Wroclaw, Poland, July 31 - August
1658               5, 2011. Proceedings},
1659  booktitle = {CADE},
1660  publisher = {Springer},
1661  series    = {LNCS},
1662  volume    = {6803},
1663  year      = {2011},
1664  isbn      = {978-3-642-22437-9},
1665  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6},
1666  bibsource = {DBLP, http://dblp.uni-trier.de}
1667}
1668
1669@article{typeffects,
1670  author    = {Jean-Pierre Talpin and
1671               Pierre Jouvelot},
1672  title     = {The Type and Effect Discipline},
1673  journal   = {Inf. Comput.},
1674  volume    = {111},
1675  number    = {2},
1676  year      = {1994},
1677  pages     = {245-296},
1678  ee        = {http://dx.doi.org/10.1006/inco.1994.1046},
1679  bibsource = {DBLP, http://dblp.uni-trier.de}
1680}
1681
1682@article{stateart,
1683  author    = {Reinhard Wilhelm and
1684               Jakob Engblom and
1685               Andreas Ermedahl and
1686               Niklas Holsti and
1687               Stephan Thesing and
1688               David B. Whalley and
1689               Guillem Bernat and
1690               Christian Ferdinand and
1691               Reinhold Heckmann and
1692               Tulika Mitra and
1693               Frank Mueller and
1694               Isabelle Puaut and
1695               Peter P. Puschner and
1696               Jan Staschulat and
1697               Per Stenstr{\"o}m},
1698  title     = {The worst-case execution-time problem---overview of methods
1699               and survey of tools},
1700  journal   = {ACM Trans. Embedded Comput. Syst.},
1701  volume    = {7},
1702  number    = {3},
1703  year      = {2008},
1704  ee        = {http://doi.acm.org/10.1145/1347375.1347389},
1705  bibsource = {DBLP, http://dblp.uni-trier.de}
1706}
1707
1708@inproceedings{bobot,
1709  year={2012},
1710  booktitle={Formal Methods and Software Engineering},
1711  volume={7635},
1712  series={Lecture Notes in Computer Science},
1713  doi={10.1007/978-3-642-34281-3_14},
1714  title={Separation Predicates: A Taste of Separation Logic in First-Order Logic},
1715  url={http://dx.doi.org/10.1007/978-3-642-34281-3_14},
1716  author={Bobot, François and Filliâtre, Jean-Christophe},
1717  pages={167-181}
1718}
1719
1720@misc
1721{ absint,
1722  url = {http://www.absint.com/ait/},
1723  author = {{AbsInt}},
1724  title = {{aiT WCET} analysis tools}
1725}
1726
1727@misc
1728{ cerco-website,
1729  url = {http://cerco.cs.unibo.it},
1730  title = {The {Certified Complexity} ({CerCo}) project web site},
1731  key = {cerco}
1732}
1733
1734@misc
1735{ jessie,
1736  url = {http://krakatoa.lri.fr/},
1737  title = {Jessie {Frama-C} plugin},
1738  key = {jessie}
1739}
1740
1741@article
1742{ asperti:user:2007,
1743  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
1744  title = {User interaction with the {Matita} proof assistant},
1745  journal = {Automated Reasoning},
1746  pages = {109--139},
1747  volume = {39},
1748  issue = {2},
1749  year = {2007}
1750}
1751
1752@article
1753{ sacerdoti-coen:tinycals:2007,
1754  author = {Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
1755  title = {{Tinycals}: Step by Step Tacticals},
1756  journal = {Electronic Notes in Theoretical Computer Science},
1757  volume = {174},
1758  number = {2},
1759  pages = {125--142},
1760  doi = {http://dx.doi.org/10.1016/j.entcs.2006.09.026},
1761  year = {2007}
1762}
1763
1764@incollection
1765{ sozeau:subset:2007,
1766  author = {Matthieu Sozeau},
1767  title = {Subset Coercions in {Coq}},
1768  booktitle = {Types for Proofs and Programs},
1769  volume = {4502},
1770  series = {Lecture Notes in Computer Science},
1771  doi = {10.1007/978-3-540-74464-1_16},
1772  pages = {237--252},
1773  year = {2007}
1774}
1775
1776@inproceedings
1777{ asperti:higher-order:2007,
1778  author = {Andrea Asperti and Enrico Tassi},
1779  title = {Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case},
1780  booktitle = {Towards Mechanized Mathematical Assistants: Calculemus},
1781  pages = {146--160},
1782  series = {Lecture Notes in Computer Science},
1783  volume = {4573},
1784  year = 2007
1785}
1786
1787@inproceedings
1788{ bove:brief:2009,
1789  author = {Ana Bove and Peter Dybjer and Ulf Norell},
1790  title = {A Brief Overview of {Agda} --- A Functional Language with Dependent Types},
1791  booktitle = {Theorem Proving in Higher-order Logics {(TPHOLs)}},
1792  year = {2009}
1793}
1794
1795@manual
1796{ coq:2004,
1797  title = {The {Coq} proof assistant reference manual},
1798  author =  {{The Coq development team}},
1799  organization = {{LogiCal Project}},
1800  note = {Version 8.0},
1801  year = {2004},
1802  url = {http://coq.inria.fr}
1803}
1804
1805@misc
1806{ cerco:2011,
1807  title = {The {CerCo} {FET-Open} project},
1808  howpublished = {\url{http://cerco.cs.unibo.it/}},
1809  year = {2011},
1810  key = {CerCo:2011}
1811}
1812
1813@inproceedings{cil02,
1814  title  = {{CIL}: Intermediate Language and Tools for Analysis and Transformation of {C} Programs},
1815  author = {George C. Necula and Scott McPeak and Shree P. Rahul and Westley Weimer},
1816  booktitle = {Compiler Construction: 11th International Conference (CC 2002)},
1817  pages = {213--228},
1818  year   = 2002,
1819  editor = {R. Nigel Horspool},
1820  volume = 2304,
1821  series = {Lecture Notes in Computer Science},
1822  publisher = {Springer},
1823  doi = {10.1007/3-540-45937-5_16}
1824}
1825
1826@Inbook{Ayache2012,
1827author="Ayache, Nicolas
1828and Amadio, Roberto M.
1829and R{\'e}gis-Gianas, Yann",
1830editor="Stoelinga, Mari{\"e}lle
1831and Pinger, Ralf",
1832title="Certifying and Reasoning on Cost Annotations in C Programs",
1833bookTitle="Formal Methods for Industrial Critical Systems: 17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings",
1834year="2012",
1835publisher="Springer Berlin Heidelberg",
1836address="Berlin, Heidelberg",
1837pages="32--46",
1838isbn="978-3-642-32469-7",
1839doi="10.1007/978-3-642-32469-7_3",
1840url="http://dx.doi.org/10.1007/978-3-642-32469-7_3"
1841}
Note: See TracBrowser for help on using the repository browser.