@inbook{19986,
  abstract     = {For non-probabilistic programs, a key question in static analysis is termination, which asks whether a given program terminates under a given initial condition. In the presence of probabilistic behaviour, there are two fundamental extensions of the termination question: (a) the almost-sure termination question, which asks whether the termination probability is 1; and (b) the bounded-time termination question, which asks whether the expected termination time is bounded. There are many active research directions to address these two questions; one important such direction is the use of martingale theory for termination analysis. In this chapter, we survey the main techniques of the martingale-based approach to the termination analysis of probabilistic programs.},
  author       = {Chatterjee, Krishnendu and Fu, Hongfei and Novotný, Petr},
  booktitle    = {Foundations of Probabilistic Programming},
  isbn         = {9781108488518},
  pages        = {221--258},
  publisher    = {Cambridge University Press},
  title        = {{Termination Analysis of Probabilistic Programs with Martingales}},
  doi          = {10.1017/9781108770750.008},
  year         = {2020},
}