---
OA_place: publisher
_id: '19986'
abstract:
- lang: eng
  text: '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.'
acknowledgement: "Krishnendu Chatterjee is supported by the Austrian Science Fund
  (FWF) NFN\r\nGrant No. S11407-N23 (RiSE/SHiNE), and COST Action GAMENET. Hongfei
  Fu\r\nis supported by the National Natural Science Foundation of China (NSFC) Grant\r\nNo.
  61802254. Petr Novotný is supported by the Czech Science Foundation grant\r\nNo.
  GJ19-15134Y."
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Hongfei
  full_name: Fu, Hongfei
  id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
  last_name: Fu
- first_name: Petr
  full_name: Novotný, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotný
citation:
  ama: 'Chatterjee K, Fu H, Novotný P. Termination Analysis of Probabilistic Programs
    with Martingales. In: <i>Foundations of Probabilistic Programming</i>. Cambridge
    University Press; 2020:221-258. doi:<a href="https://doi.org/10.1017/9781108770750.008">10.1017/9781108770750.008</a>'
  apa: Chatterjee, K., Fu, H., &#38; Novotný, P. (2020). Termination Analysis of Probabilistic
    Programs with Martingales. In <i>Foundations of Probabilistic Programming</i>
    (pp. 221–258). Cambridge University Press. <a href="https://doi.org/10.1017/9781108770750.008">https://doi.org/10.1017/9781108770750.008</a>
  chicago: Chatterjee, Krishnendu, Hongfei Fu, and Petr Novotný. “Termination Analysis
    of Probabilistic Programs with Martingales.” In <i>Foundations of Probabilistic
    Programming</i>, 221–58. Cambridge University Press, 2020. <a href="https://doi.org/10.1017/9781108770750.008">https://doi.org/10.1017/9781108770750.008</a>.
  ieee: K. Chatterjee, H. Fu, and P. Novotný, “Termination Analysis of Probabilistic
    Programs with Martingales,” in <i>Foundations of Probabilistic Programming</i>,
    Cambridge University Press, 2020, pp. 221–258.
  ista: 'Chatterjee K, Fu H, Novotný P. 2020.Termination Analysis of Probabilistic
    Programs with Martingales. In: Foundations of Probabilistic Programming. , 221–258.'
  mla: Chatterjee, Krishnendu, et al. “Termination Analysis of Probabilistic Programs
    with Martingales.” <i>Foundations of Probabilistic Programming</i>, Cambridge
    University Press, 2020, pp. 221–58, doi:<a href="https://doi.org/10.1017/9781108770750.008">10.1017/9781108770750.008</a>.
  short: K. Chatterjee, H. Fu, P. Novotný, in:, Foundations of Probabilistic Programming,
    Cambridge University Press, 2020, pp. 221–258.
corr_author: '1'
date_created: 2025-07-10T13:28:51Z
date_published: 2020-11-18T00:00:00Z
date_updated: 2025-09-23T12:10:25Z
day: '18'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1017/9781108770750.008
file:
- access_level: open_access
  checksum: 28ece115e8d2d9263e253a598e7caef2
  content_type: application/pdf
  creator: dernst
  date_created: 2025-09-23T12:03:09Z
  date_updated: 2025-09-23T12:03:09Z
  file_id: '20380'
  file_name: 2020_ProbProgramming_Chatterjee.pdf
  file_size: 316681
  relation: main_file
  success: 1
file_date_updated: 2025-09-23T12:03:09Z
has_accepted_license: '1'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '11'
oa: 1
oa_version: Published Version
page: 221-258
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
publication: Foundations of Probabilistic Programming
publication_identifier:
  eisbn:
  - '9781108770750'
  isbn:
  - '9781108488518'
publication_status: published
publisher: Cambridge University Press
quality_controlled: '1'
status: public
title: Termination Analysis of Probabilistic Programs with Martingales
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2020'
...