M. Aab-+-14]-roberto, N. Amadio, F. Ayache, J. Bobot, B. Boender et al., Certified complexity (CerCo). In Foundational and Practical Aspects of Resource Analysis, Lecture Notes in Computer Science, vol.8552, pp.1-18, 2014.

P. Aag-+-12]-elvira-albert, S. Arenas, G. Genaim, D. Puebla, and . Zanardini, Cost analysis of object-oriented bytecode programs, Theoretical Computer Science, vol.413, issue.1, pp.142-159, 2012.

N. Ayache, R. M. Amadio, and Y. Régis-gianas, Certifying and reasoning on cost annotations in C programs, Formal Methods for Industrial Critical Systems, vol.7437, pp.32-46, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00702665

M. A. Akra and L. Bazzi, On the solution of linear recurrence equations, Comp. Opt. and Appl, vol.10, issue.2, pp.195-210, 1998.

, Deductive Software Verification -The KeY Book -From Theory to Practice, Lecture Notes in Computer Science, vol.10001, 2016.

D. E. , A. , and S. Genaim, On the limits of the classical approach to cost analysis, Static Analysis, pp.405-421, 2012.

R. Affeldt, C. Cohen, and D. Rouhling, Formalization techniques for asymptotic reasoning in classical analysis, Journal of Formalized Reasoning, vol.11, issue.1, pp.43-76, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01719918

J. Avigad and K. Donnelly, Formalizing O notation in Isabelle/HOL, International Joint Conference on Automated Reasoning, vol.3097, pp.357-371, 2004.

M. Avanzini and U. Dal-lago, Automating sized-type inference for complexity analysis, Proc. ACM Program. Lang, vol.1, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01639200

M. Avanzini, U. D. Lago, and G. Moser, Analysing the complexity of functional programs: Higher-order meets first-order, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pp.152-164, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01231809

G. Afg-+-11]-michaël-armand, B. Faure, C. Grégoire, L. Keller, B. Thery et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, CPP -Certified Programs and Proofs -First International Conference -2011, vol.7086, pp.135-150, 2011.

M. Avanzini and G. Moser, A combination framework for complexity, 24th International Conference on Rewriting Techniques and Applications, RTA 2013, pp.55-70, 2013.

M. Abdulaziz, K. Mehlhorn, and T. Nipkow, Trustworthy Graph Algorithms (Invited Talk), 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), vol.138, 2019.

R. Amadio and Y. Régis-gianas, Certifying and reasoning on cost annotations of functional programs, Foundational and Practical Aspects of Resource Analysis, vol.7177, pp.72-89, 2011.

R. Atkey, Amortised resource analysis with separation logic, Logical Methods in Computer Science, vol.7, issue.2, p.17, 2011.

. Bef-+-14]-marc, F. Brockschmidt, S. Emmes, C. Falke, J. Fuhs et al., Alternating runtime and size complexity analysis of integer programs, Tools and Algorithms for the Construction and Analysis of Systems, pp.140-155, 2014.

R. Benzinger, Automated higher-order complexity analysis, Theor. Comput. Sci, vol.318, issue.1-2, pp.79-103, 2004.

M. A. Bender, J. T. Fineman, S. Gilbert, and R. E. Tarjan, A new approach to incremental cycle detection and related problems, ACM Transactions on Algorithms, vol.12, issue.2, 2016.

A. Bizjak, D. Gratzer, R. Krebbers, and L. Birkedal, Iron: Managing obligations in higher-order concurrent separation logic, Proc. ACM Program. Lang, vol.3, 2019.

R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács, Abc: Algebraic bound computation for loops, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp.103-118, 2010.

J. L. Bentley, D. Haken, and J. B. Saxe, A general method for solving divide-and-conquer recurrences, SIGACT News, vol.12, issue.3, pp.36-44, 1980.

L. Bulwahn, A. Krauss, F. Haftmann, L. Erkök, and J. Matthews, Imperative functional programming with Isabelle/HOL, Theorem Proving in Higher Order Logics (TPHOLs), vol.5170, pp.134-149, 2008.

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A userfriendly library of real analysis for Coq, Mathematics in Computer Science, vol.9, issue.1, pp.41-62, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00860648

N. Bourbaki, General Topology, 1995.

Q. Carbonneaux, Modular and Certified Resource-Bound Analyses, 2018.

C. Ccl-+-18]-ran-chen, J. Cohen, S. Lévy, L. Merz, and . Théry, Formal proofs of Tarjan's algorithm in Why3, Coq, and Isabelle. Manuscript, 2018.

A. Charguéraud, The TLC coq library

A. Charguéraud, Characteristic Formulae for Mechanized Program Verification, 2010.

A. Charguéraud, The optimal fixed point combinator, Interactive Theorem Proving (ITP), vol.6172, pp.195-210, 2010.

A. Charguéraud, Characteristic formulae for the verification of imperative programs, 2013.

A. Charguéraud, The cfml2 framework, 2019.

A. Charguéraud, The CFML tool and library, 2019.

Q. Carbonneaux, J. Hoffmann, T. Ramananandro, and Z. Shao, End-to-end verification of stack-space bounds for C programs, Programming Language Design and Implementation (PLDI), pp.270-281, 2014.

Q. Carbonneaux, J. Hoffmann, T. Reps, and Z. Shao, Automated resource analysis with Coq proof objects, Computer Aided Verification (CAV), vol.10427, pp.64-85

. Springer, , 2017.

Q. Carbonneaux, J. Hoffmann, and Z. Shao, Compositional certified resource bounds, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15, pp.467-478, 2015.

R. Chen and J. Lévy, A semi-automatic proof of strong connectivity, Verified Software: Theories, Tools and Experiments, vol.10712, pp.49-65, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01632947

H. Thomas, C. E. Cormen, R. L. Leiserson, C. Rivest, and . Stein, , 2009.

C. Cohen, Formalized algebraic numbers: construction and first-order theory, 2012.
URL : https://hal.archives-ouvertes.fr/pastel-00780446

D. C. Cooper, Theorem proving in arithmetic without multiplication, Machine Intelligence 7, pp.91-99, 1972.

A. Charguéraud and F. Pottier, Temporary read-only permissions for separation logic, European Symposium on Programming, vol.10201, pp.260-286, 2017.

A. Charguéraud and F. Pottier, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Journal of Automated Reasoning, 2017.

. Eu, Effective DoS attacks against web application platforms

K. Crary and S. Weirich, Resource bound certification, Principles of Programming Languages (POPL), pp.184-198, 2000.

N. Anders-danielsson, Lightweight semiformal time complexity analysis for purely functional data structures, Principles of Programming Languages (POPL), 2008.

N. Danner, D. R. Licata, and R. Ramyaa, Denotational cost semantics for functional languages with inductive types, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pp.140-151, 2015.

N. Danner, J. Paykin, and J. S. Royer, A static cost analysis for a higher-order language, Programming Languages Meets Program Verification (PLPV), pp.25-34, 2013.

M. Eberl, Proving divide and conquer complexities in Isabelle/HOL, Journal of Automated Reasoning, vol.58, issue.4, pp.483-508, 2017.

M. Eberl, Verified solving and asymptotics of linear recurrences, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pp.27-37, 2019.

Y. Forster and F. Kunze, A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus, 10th International Conference on Interactive Theorem Proving (ITP 2019), vol.141, pp.1-17, 2019.

J. , C. Filliâtre, and P. Letouzey, Functors for proofs and programs, European Symposium on Programming, vol.2986, pp.370-384, 2004.

A. Flores, -. Montoya, and R. Hähnle, Resource analysis of complex programs with cost equations, Programming Languages and Systems, pp.275-295, 2014.

J. , C. Filliâtre, and A. Paskevich, Why3-where programs meet provers, European Symposium on Programming, vol.7792, pp.125-128, 2013.

A. Guéneau, A. Charguéraud, and F. Pottier, A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification, European Symposium on Programming, vol.10801, pp.533-560, 2018.

A. Guéneau, J. Jourdan, A. Charguéraud, and F. Pottier, The verified incremental cycle detection library, 2019.

S. Gulwani, K. K. Mehra, and T. M. Chilimbi, SPEED: precise and efficient static estimation of program computational complexity, Principles of Programming Languages (POPL), pp.127-139, 2009.

A. Guéneau, M. O. Myreen, R. Kumar, and M. Norrish, Verified characteristic formulae for CakeML, European Symposium on Programming, vol.10201, pp.584-610, 2017.

A. Guéneau and F. Pottier, The minicooper library, 2018.

, Armaël Guéneau. Coq issue #6723

, Armaël Guéneau. Coq issue #6726

A. Guéneau, Manual of the procrastination library, 2018.

A. Guéneau, The bigO library, 2018.

A. Guéneau, The procrastination library, 2018.

A. Guéneau, Dune pull request #1955, 2019.

S. Gulwani, SPEED: symbolic complexity bound analysis, Computer Aided Verification (CAV), vol.5643, pp.51-62, 2009.

J. Hoffmann, K. Aehlig, and M. Hofmann, Multivariate amortized resource analysis, ACM Transactions on Programming Languages and Systems, vol.34, issue.3, 2012.

J. Hoffmann, K. Aehlig, and M. Hofmann, Resource aware ML, Computer Aided Verification (CAV), vol.7358, pp.781-786, 2012.

J. Harrison, Handbook of Practical Logic and Automated Reasoning, 2009.

J. Hoffmann, A. Das, and S. Weng, Towards automatic resource bound analysis for OCaml, Principles of Programming Languages (POPL), pp.359-373, 2017.

J. Hoffmann and M. Hofmann, Amortized resource analysis with polynomial potential, European Symposium on Programming, vol.6012, pp.287-306, 2010.

J. Hölzl, F. Immler, and B. Huffman, Type classes and filters for mathematical analysis in isabelle/hol, Interactive Theorem Proving, pp.279-294, 2013.

M. Hofmann and S. Jost, Static prediction of heap space usage for first-order functional programs, Principles of Programming Languages (POPL), pp.185-197, 2003.

P. L. Maximilian, P. Haslbeck, and . Lammich, Refinement with Time -Refining the Run-Time of Algorithms in Isabelle/HOL, 10th International Conference on Interactive Theorem Proving (ITP 2019), vol.141, pp.1-20, 2019.

M. Hofmann and G. Moser, Amortised resource analysis and typed polynomial interpretations, Rewriting and Typed Lambda Calculi, pp.272-286, 2014.

J. Hoffmann, M. Marmar, and Z. Shao, Quantitative reasoning for proving lock-freedom, Logic in Computer Science (LICS), pp.124-133, 2013.

P. L. Maximilian, T. Haslbeck, and . Nipkow, Hoare logics for time bounds: A study in meta theory, Tools and Algorithms for Construction and Analysis of Systems (TACAS), vol.10805, pp.155-171, 2018.

M. Hofmann, Linear types and non size-increasing polynomial time computation, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS '99, p.464, 1999.

J. E. Hopcroft, Computer science: The emergence of a discipline, Communications of the ACM, vol.30, issue.3, pp.198-202, 1987.

R. R. Howell, On asymptotic notation with multiple variables, 2008.

B. Holland, R. Ganesh, P. Santhanam, S. Awadhutkar, and . Kothari, Statically-informed dynamic analysis tools to detect algorithmic complexity vulnerabilities, Source Code Analysis and Manipulation (SCAM), pp.79-84, 2016.

N. Iqbal and O. Hasan, Umair Siddique, and Falah Awwd. Formalization of asymptotic notations in hol4, IEEE 4th International Conference on Computer and Communication Systems (ICCCS), 2019.

S. Jost, K. Hammond, H. Loidl, and M. Hofmann, Static determination of quantitative resource usage for higher-order programs, Principles of Programming Languages (POPL), pp.223-236, 2010.

. Jkj-+-18]-ralf, R. Jung, J. Krebbers, A. Jourdan, L. Bizjak et al., Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Journal of Functional Programming, vol.28, issue.20, 2018.

J. Jourdan, Coq pull request #89, 2015.

D. Kahn and J. Hoffmann, Exponential automatic amortized resource analysis, 2019.

R. Krueger, P. Rudnicki, and P. Shelley, Asymptotic notation. Part I: theory, Journal of Formalized Mathematics, vol.11, 1999.

D. Kroening and O. Strichman, Decision procedures -An algorithmic point of view, 2008.

R. Krebbers, A. Timany, and L. Birkedal, Interactive proofs in higherorder concurrent separation logic, Principles of Programming Languages (POPL, 2017.

P. Lammich, Verified efficient implementation of Gabow's strongly connected component algorithm, Interactive Theorem Proving (ITP), vol.8558, pp.325-340, 2014.

T. Leighton, Notes on better master theorems for divide-and-conquer recurrences, 1996.

B. Lichtman and J. Hoffmann, Arrays and References in Resource Aware ML, 2nd International Conference on Formal Structures for Computation and Deduction, vol.84, pp.1-26, 2017.

P. Lammich and R. Meis, A separation logic framework for Imperative HOL. Archive of Formal Proofs, 2012.

C. Lemieux, R. Padhye, K. Sen, and D. Song, PerfFuzz: Automatically generating pathological inputs, International Symposium on Software Testing and Analysis (ISSTA), pp.254-265, 2018.

P. Lammich and S. R. Sefidgar, Formalizing the edmonds-karp algorithm. Archive of Formal Proofs, 2016.

J. A. Mccarthy, B. Fetscher, M. S. New, D. Feltey, and R. B. Findler, A Coq library for internal verification of runningtimes, Functional and Logic Programming, vol.9613, pp.144-162, 2016.

G. Mével, J. Jourdan, and F. Pottier, Time credits and time receipts in Iris, European Symposium on Programming, vol.11423, pp.1-27

. Springer, , 2019.

R. Madhavan, S. Kulal, and V. Kuncak, Contract-based resource verification for higher-order functions with memoization, Principles of Programming Languages (POPL), pp.330-343, 2017.

R. Mudduluru and . Murali-krishna-ramanathan, Efficient flow profiling for detecting performance bugs, International Symposium on Software Testing and Analysis (ISSTA), pp.413-424, 2016.

P. Müller, M. Schwerhoff, and A. J. Summers, Viper: A verification infrastructure for permission-based reasoning, Dependable Software Systems Engineering, pp.104-125, 2017.

T. Nipkow and H. Brinkop, Amortized complexity verified, Journal of Automated Reasoning, vol.62, issue.3, pp.367-391, 2019.

H. and R. Nielson, Hoare Logic's for Run-time Analysis of Programs, 1984.

. Hanne-riis-nielson, A hoare-like proof system for analysing the computation time of programs, Sci. Comput. Program, vol.9, issue.2, pp.107-136, 1987.

T. Nipkow, Amortized complexity verified, Interactive Theorem Proving (ITP), vol.9236, pp.310-324

. Springer, , 2015.

Y. Noller, R. Kersten, and C. S. P?s?reanu, Badger: Complexity analysis with fuzzing and symbolic execution, Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp.322-332, 2018.

R. Hanne, F. Nielson, and . Nielson, Semantics with applications: an appetizer, 2007.

O. Olivo, I. Dillig, and C. Lin, Static detection of asymptotic performance bugs in collection traversals, Programming Language Design and Implementation (PLDI), pp.369-378, 2015.

C. Okasaki, Purely Functional Data Structures, 1999.

M. Parkinson and G. Bierman, Separation logic and abstraction, Principles of Programming Languages (POPL), pp.247-258, 2005.

F. Pottier, Depth-first search and strong connectivity in Coq, Journées Françaises des Langages Applicatifs (JFLA), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01096354

A. Pilkiewicz and F. Pottier, The essence of monotonic state, Types in Language Design and Implementation (TLDI), 2011.
URL : https://hal.archives-ouvertes.fr/hal-01081193

T. Petsios, J. Zhao, A. D. Keromytis, and S. Jana, Slowfuzz: Automated domain-independent detection of algorithmic complexity vulnerabilities, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS '17, pp.2155-2168, 2017.

G. Rbg-+-18]-ivan-radi?ek, M. Barthe, D. Gaboardi, F. Garg, and . Zuleger, Monadic refinements for relational cost analysis, Proc. ACM Program. Lang, vol.2, p.32, 2018.

J. C. Reynolds, Separation logic: A logic for shared mutable data structures, Logic in Computer Science (LICS), pp.55-74, 2002.

D. M. Russinoff, A mechanically verified incremental garbage collector, Formal Aspects of Computing, vol.6, issue.4, pp.359-390, 1994.

M. Sozeau and N. Oury, First-class type classes, Theorem Proving in Higher Order Logics (TPHOL), pp.278-293, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00628864

M. Sozeau and N. Tabareau, Universe polymorphism in Coq, Interactive Theorem Proving (ITP), vol.8558, pp.499-514, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00974721

J. Street, Dune: A composable build system, 2018.

N. Swamy, J. Weinberger, C. Schlesinger, J. Chen, and B. Livshits, Verifying higher-order programs with the dijkstra monad, Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, pp.387-398, 2013.

F. Moritz-sinn, H. Zuleger, and . Veith, A simple and scalable static analysis for bound analysis and amortized complexity analysis, Computer Aided Verification, pp.745-761, 2014.

. Robert-endre-tarjan, Amortized computational complexity. SIAM Journal on Algebraic and Discrete Methods, vol.6, issue.2, pp.306-318, 1985.

. Robert-endre-tarjan, Algorithmic design, Communications of the ACM, vol.30, issue.3, pp.204-212, 1987.

L. Théry, Simplifying Polynomial Expressions in a Proof Assistant, INRIA, 2005.

, The Coq development team. The Coq Manual, Miscellaneous extensions: Program Derivation, 2019.

, The Coq development team. The Coq Proof Assistant, 2019.

M. Luca-della-toffola, T. R. Pradel, and . Gross, Synthesizing programs that expose performance bottlenecks, Code Generation and Optimization (CGO), pp.314-326, 2018.

P. B. Vasconcelos and K. Hammond, Inferring cost equations for recursive, polymorphic and higher-order functional programs, Proceedings of the 15th International Conference on Implementation of Functional Languages, IFL'03, pp.86-101, 2004.

J. Eelis-van-der-weegen and . Mckinna, A machine-checked proof of the average-case complexity of Quicksort in Coq, Types for Proofs and Programs, vol.5497, pp.256-271, 2008.

P. Wang, Type System for Resource Bounds with Type-Preserving Compilation, 2018.

. Wcf-+-18]-jiayi, J. Wei, Y. Chen, K. Feng, I. Ferles et al., Singularity: Pattern fuzzing for worst case complexity, Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp.213-223, 2018.

J. Wilhelm, A. Engblom, N. Ermedahl, S. Holsti, D. Thesing et al., The worst-case execution-time problemoverview of methods and survey of tools, Staschulat, and Per Stenström, vol.7, p.53, 2008.

B. Wegbreit, Mechanical program analysis, Communications of the ACM, vol.18, issue.9, pp.528-539, 1975.

P. Wang, D. Wang, and A. Chlipala, TiML: A functional language for practical complexity analysis with invariants, Proceedings of the ACM on Programming Languages, vol.1, 2017.

F. Zuleger, S. Gulwani, M. Sinn, and H. Veith, Bound analysis of imperative programs with the size-change abstraction, Static Analysis, pp.280-297, 2011.

T. Zimmermann and H. Herbelin, Coq's prolog and application to defining semi-automatic tactics, Type Theory Based Tools (TTT, 2017.

B. Zhan and M. P. Haslbeck, Verifying asymptotic time complexity of imperative programs in Isabelle, International Joint Conference on Automated Reasoning, 2018.

. Bohua-zhan, Efficient verification of imperative programs using auto2, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.23-40, 2018.