S. Agrawal, K. Chatterjee, and P. Novotný, Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs, PACMPL, vol.2, pp.1-34, 2018.

E. Albert, P. Gordillo, A. Rubio, and I. Sergey, Running on Fumes, Lecture Notes in Computer Science, vol.11847, pp.63-78, 2019.

C. Alias, A. Darte, P. Feautrier, and L. Gonnord, Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs, Static Analysis, vol.6337, pp.117-133, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00523298

M. Avanzini, U. Dal-lago, and A. Ghyselen, Type-Based Complexity Analysis of Probabilistic Functional Programs, 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2019.
URL : https://hal.archives-ouvertes.fr/hal-02103943

M. Avanzini, U. Dal-lago, and A. Yamada, On probabilistic term rewriting, Science of Computer Programming, vol.185, p.102338, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02381877

M. Avanzini, G. Moser, and M. Schaper, TcT: Tyrolean Complexity Tool, Tools and Algorithms for the Construction and Analysis of Systems, pp.407-423, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01392188

M. Avanzini, U. Dal-lago, and A. Yamada, On probabilistic term rewriting, Science of Computer Programming, vol.185, p.102338, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02381877

G. Barthe, B. Grégoire, and S. Zanella-béguelin, Formal certification of code-based cryptographic proofs, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '09, pp.90-101, 2008.

A. Ben-amram, Monotonicity Constraints for Termination in the Integer Domain, Logical Methods in Computer Science, vol.7, issue.3, pp.1-43, 2011.

A. Ben-amram, Mortality of iterated piecewise affine functions over the integers: Decidability and complexity, Computability, vol.4, issue.1, pp.19-56, 2015.

A. M. Ben-amram and G. W. Hamilton, Tight Worst-Case Bounds for Polynomial Loop Programs, Lecture Notes in Computer Science, vol.11425, pp.80-97, 2019.

A. M. Ben-amram and L. Kristiansen, ON THE EDGE OF DECIDABILITY IN COMPLEXITY ANALYSIS OF LOOP PROGRAMS, International Journal of Foundations of Computer Science, vol.23, issue.07, pp.1451-1464, 2012.

O. Bournez and F. Garnier, Proving Positive Almost-Sure Termination, Proc. of 16 th RTA, vol.3467, pp.323-337, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000522

T. Brázdil, S. Kiefer, A. Ku?era, and I. Huta?ová-va?eková, Runtime analysis of probabilistic programs with unbounded recursion, Journal of Computer and System Sciences, vol.81, issue.1, pp.288-310, 2015.

F. Breuvart and U. D. Lago, On Intersection Types and Probabilistic Lambda Calculi, Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, vol.8, pp.1-8, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01926420

M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl, Alternating Runtime and Size Complexity Analysis of Integer Programs, Tools and Algorithms for the Construction and Analysis of Systems, vol.8413, pp.140-155, 2014.

M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl, Analyzing Runtime and Size Complexity of Integer Programs, ACM Transactions on Programming Languages and Systems, vol.38, issue.4, pp.1-50, 2016.

Q. Carbonneaux, J. Hoffmann, and Z. Shao, Compositional certified resource bounds, ACM SIGPLAN Notices, vol.50, issue.6, pp.467-478, 2015.

O. Celiku and A. Mciver, Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs, FM 2005: Formal Methods, vol.3582, pp.107-122, 2005.

A. Chakarov and S. Sankaranarayanan, Probabilistic Program Analysis with Martingales, Computer Aided Verification, vol.8044, pp.511-526, 2013.

A. Chakarov and S. Sankaranarayanan, Expectation Invariants for Probabilistic Program Loops as Fixed Points, Static Analysis, pp.85-100, 2014.

K. Chatterjee, H. Fu, and A. K. Goharshady, Termination Analysis of Probabilistic Programs Through Positivstellensatz?s, Computer Aided Verification, vol.9779, pp.3-22, 2016.

K. Chatterjee, H. Fu, and A. Murhekar, Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds, Computer Aided Verification, vol.10426, pp.118-139, 2017.

K. Chatterjee, P. Novotný, and Ð. ?ikeli?, Stochastic invariants for probabilistic termination, ACM SIGPLAN Notices, vol.52, issue.1, pp.145-160, 2017.

J. Cohen and C. Zuckerman, Two languages for estimating program efficiency, Communications of the ACM, vol.17, issue.6, pp.301-308, 1974.

E. Contejean, C. Marché, A. Tomás, X. Urbain, R. Cousot et al., Mechanically Proving Termination Using Polynomial Interpretations, Proc. of 11 th CC, vol.34, pp.159-178, 2002.
URL : https://hal.archives-ouvertes.fr/hal-01984434

J. Dean and S. Ghemawat, MapReduce, Communications of the ACM, vol.51, issue.1, pp.107-113, 2008.

I. Dillig, T. Dillig, and A. Aiken, Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis, Static Analysis, pp.236-252, 2010.

J. Esparza, A. Kucera, and R. Mayr, Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.117-126

T. Fiedor, L. Holík, A. Rogalewicz, M. Sinn, T. Vojnar et al., From Shapes to Amortized Complexity, Lecture Notes in Computer Science, vol.10747, pp.205-225, 2017.

F. Frohn and J. Giesl, Complexity Analysis for Java with AProVE, Lecture Notes in Computer Science, vol.10510, pp.85-101, 2017.

C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-kamp, R. Thiemann et al., SAT Solving for Termination Analysis with Polynomial Interpretations, Theory and Applications of Satisfiability Testing ? SAT 2007, vol.4501, pp.340-354

T. Gehr, S. Misailovic, and M. Vechev, PSI: Exact Symbolic Inference for Probabilistic Programs, Computer Aided Verification, vol.9779, pp.62-83, 2016.

S. Gulwani, K. K. Mehra, and T. M. Chilimbi, SPEED, ACM SIGPLAN Notices, vol.44, issue.1, pp.127-139, 2009.

S. Gulwani and A. Tiwari, Combining abstract interpreters, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation - PLDI '06, pp.376-386, 2006.

S. Gulwani and F. Zuleger, The reachability-bound problem, ACM SIGPLAN Notices, vol.45, issue.6, pp.292-304, 2010.

D. Handelman, Representing polynomials by positive linear functions on compact convex polyhedra, Pacific Journal of Mathematics, vol.132, issue.1, pp.35-62, 1988.

M. D. Hill and M. R. Marty, Amdahl's Law in the Multicore Era, Computer, vol.41, issue.7, pp.33-38, 2008.

N. Hirokawa and G. Moser, Automated Complexity Analysis Based on the Dependency Pair Method, Automated Reasoning, vol.5195, pp.364-379

J. Hoffmann, A. Das, and S. Weng, Towards automatic resource bound analysis for OCaml, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages - POPL 2017, pp.359-373, 2017.

N. D. Jones and L. Kristiansen, A flow calculus of mwp -bounds for complexity analysis, ACM Transactions on Computational Logic, vol.10, issue.4, pp.1-41, 2009.

B. L. Kaminski and J. Katoen, A weakest pre-expectation semantics for mixed-sign expectations, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp.1-12, 2017.

B. L. Kaminski, J. Katoen, C. Matheja, and F. Olmedo, Weakest Precondition Reasoning for Expected Run?Times of Probabilistic Programs, Programming Languages and Systems, vol.9632, pp.364-389, 2016.

B. L. Kaminski, J. Katoen, C. Matheja, and F. Olmedo, Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms, Journal of the ACM, vol.65, issue.5, pp.1-68, 2018.

B. L. Kaminski and J. Katoen, On the Hardness of Almost?Sure Termination, Mathematical Foundations of Computer Science 2015, pp.307-318, 2015.

J. Katoen, The Probabilistic Model Checking Landscape, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '16, pp.31-45, 2016.

J. Katoen, A. K. Mciver, L. A. Meinicke, and C. C. Morgan, Linear-Invariant Generation for Probabilistic Programs:, Static Analysis, vol.6337, pp.390-406, 2010.

C. Kim and A. K. Agrawala, Analysis of the fork-join queue, IEEE Transactions on Computers, vol.38, issue.2, pp.250-255, 1989.

D. Kozen, Semantics of probabilistic programs, Journal of Computer and System Sciences, vol.22, issue.3, pp.328-350, 1981.

D. Kozen, A probabilistic PDL, Journal of Computer and System Sciences, vol.30, issue.2, pp.162-178, 1985.

A. Mciver, C. Morgan, B. L. Kaminski, and J. Katoen, A new proof rule for almost-sure termination, Proceedings of the ACM on Programming Languages, vol.2, issue.POPL, pp.1-28, 2018.

D. A. Menascé, Response-time analysis of composite web services, IEEE Internet Computing, vol.8, issue.1, pp.90-92, 2004.

M. Mitzenmacher and E. Upfal, Probability and Computing, Probability and Computing: Randomized Algorithms and Probabilistic Analysis, 2005.

D. Monniaux, An Abstract Analysis of the Probabilistic Termination of Programs, Proc. of 8 th SAS, vol.2126, 2001.

. Springer, , pp.111-126

G. Moser and M. Schaper, From Jinja Bytecode to Term Rewriting: A Complexity Reflecting Transformation, Part, vol.261, pp.116-143, 2018.

V. C. Ngo, Q. Carbonneaux, and J. Hoffmann, Bounded expectations: resource analysis for probabilistic programs, ACM SIGPLAN Notices, vol.53, issue.4, pp.496-512, 2018.

V. C. Ngo, M. Dehesa-azuara, M. Fredrikson, and J. Hoffmann, Verifying and Synthesizing Constant-Resource Implementations with Types, Proc. of 38 th S&P, pp.710-728, 2017.

F. Olmedo, B. L. Kaminski, J. Katoen, and C. Matheja, Reasoning about Recursive Probabilistic Programs, Proc. of 31 nd LICS, pp.672-681, 2016.

A. Podelski and A. Rybalchenko, A Complete Method for the Synthesis of Linear Ranking Functions, Lecture Notes in Computer Science, vol.2937, pp.239-251, 2004.

R. Sedgewick and P. Flajolet, An Introduction to the Analysis of Algorithms, 1996.

M. Sinn, F. Zuleger, and H. Veith, A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis, Computer Aided Verification, vol.8559, pp.745-761, 2014.

M. Sinn, F. Zuleger, and H. Veith, Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints, Journal of Automated Reasoning, vol.59, issue.1, pp.3-45, 2017.

T. Takisaka, Y. Oyabu, N. Urabe, and I. Hasuo, Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs, Automated Technology for Verification and Analysis, vol.11138, pp.476-493, 2018.

D. Wang, J. Hoffmann, and T. W. Reps, PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs, Proc. of 39 th PLDI, pp.513-528, 2018.

P. Wang, H. Fu, A. K. Goharshady, K. Chatterjee, X. Qin et al., Cost analysis of nondeterministic probabilistic programs, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI 2019, pp.204-220, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02016018

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

B. Wegbreit, Verifying Program Performance, JACM, vol.23, pp.691-699, 1976.

R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing et al., The worst-case execution-time problem?overview of methods and survey of tools, ACM Transactions on Embedded Computing Systems, vol.7, issue.3, pp.1-53, 2008.

R. Wilhelm and D. Grund, Computation takes time, but how much?, Communications of the ACM, vol.57, issue.2, pp.94-103, 2014.

G. Winskel, Introduction to operational semantics, The Formal Semantics of Programming Languages, 1993.