---
_id: '6780'
abstract:
- lang: eng
  text: "In this work, we consider the almost-sure termination problem for probabilistic
    programs that asks whether a\r\ngiven probabilistic program terminates with probability
    1. Scalable approaches for program analysis often\r\nrely on modularity as their
    theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule)\r\nof
    Floyd-Hoare logic provides the foundation for modular analysis. Extension of this
    rule to almost-sure\r\ntermination of probabilistic programs is quite tricky,
    and a probabilistic variant was proposed in [16]. While the\r\nproposed probabilistic
    variant cautiously addresses the key issue of integrability, we show that the
    proposed\r\nmodular rule is still not sound for almost-sure termination of probabilistic
    programs.\r\nBesides establishing unsoundness of the previous rule, our contributions
    are as follows: First, we present a\r\nsound modular rule for almost-sure termination
    of probabilistic programs. Our approach is based on a novel\r\nnotion of descent
    supermartingales. Second, for algorithmic approaches, we consider descent supermartingales\r\nthat
    are linear and show that they can be synthesized in polynomial time. Finally,
    we present experimental\r\nresults on a variety of benchmarks and several natural
    examples that model various types of nested while\r\nloops in probabilistic programs
    and demonstrate that our approach is able to efficiently prove their almost-sure\r\ntermination
    property"
article_number: '129'
article_processing_charge: No
arxiv: 1
author:
- first_name: Mingzhang
  full_name: Huang, Mingzhang
  last_name: Huang
- first_name: Hongfei
  full_name: Fu, Hongfei
  last_name: Fu
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
  full_name: Goharshady, Amir Kafshdar
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
citation:
  ama: 'Huang M, Fu H, Chatterjee K, Goharshady AK. Modular verification for almost-sure
    termination of probabilistic programs. In: <i>Proceedings of the 34th ACM International
    Conference on Object-Oriented Programming, Systems, Languages, and Applications
    </i>. Vol 3. ACM; 2019. doi:<a href="https://doi.org/10.1145/3360555">10.1145/3360555</a>'
  apa: 'Huang, M., Fu, H., Chatterjee, K., &#38; Goharshady, A. K. (2019). Modular
    verification for almost-sure termination of probabilistic programs. In <i>Proceedings
    of the 34th ACM International Conference on Object-Oriented Programming, Systems,
    Languages, and Applications </i> (Vol. 3). Athens, Greece: ACM. <a href="https://doi.org/10.1145/3360555">https://doi.org/10.1145/3360555</a>'
  chicago: Huang, Mingzhang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar
    Goharshady. “Modular Verification for Almost-Sure Termination of Probabilistic
    Programs.” In <i>Proceedings of the 34th ACM International Conference on Object-Oriented
    Programming, Systems, Languages, and Applications </i>, Vol. 3. ACM, 2019. <a
    href="https://doi.org/10.1145/3360555">https://doi.org/10.1145/3360555</a>.
  ieee: M. Huang, H. Fu, K. Chatterjee, and A. K. Goharshady, “Modular verification
    for almost-sure termination of probabilistic programs,” in <i>Proceedings of the
    34th ACM International Conference on Object-Oriented Programming, Systems, Languages,
    and Applications </i>, Athens, Greece, 2019, vol. 3.
  ista: 'Huang M, Fu H, Chatterjee K, Goharshady AK. 2019. Modular verification for
    almost-sure termination of probabilistic programs. Proceedings of the 34th ACM
    International Conference on Object-Oriented Programming, Systems, Languages, and
    Applications . OOPSLA: Object-oriented Programming, Systems, Languages and Applications
    vol. 3, 129.'
  mla: Huang, Mingzhang, et al. “Modular Verification for Almost-Sure Termination
    of Probabilistic Programs.” <i>Proceedings of the 34th ACM International Conference
    on Object-Oriented Programming, Systems, Languages, and Applications </i>, vol.
    3, 129, ACM, 2019, doi:<a href="https://doi.org/10.1145/3360555">10.1145/3360555</a>.
  short: M. Huang, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Proceedings of the
    34th ACM International Conference on Object-Oriented Programming, Systems, Languages,
    and Applications , ACM, 2019.
conference:
  end_date: 2019-10-25
  location: Athens, Greece
  name: 'OOPSLA: Object-oriented Programming, Systems, Languages and Applications'
  start_date: 2019-10-23
date_created: 2019-08-09T09:54:20Z
date_published: 2019-10-01T00:00:00Z
date_updated: 2026-09-13T22:31:00Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3360555
ec_funded: 1
external_id:
  arxiv:
  - '1901.06087'
file:
- access_level: open_access
  checksum: 3482d8ace6fb4991eb7810e3b70f1b9f
  content_type: application/pdf
  creator: akafshda
  date_created: 2019-08-12T15:40:57Z
  date_updated: 2020-07-14T12:47:40Z
  file_id: '6807'
  file_name: oopsla-2019.pdf
  file_size: 1024643
  relation: main_file
- access_level: open_access
  checksum: 4e5a6fb2b59a75222a4e8335a5a60eac
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-12T15:15:14Z
  date_updated: 2020-07-14T12:47:40Z
  file_id: '7821'
  file_name: 2019_ACM_Huang.pdf
  file_size: 538579
  relation: main_file
file_date_updated: 2020-07-14T12:47:40Z
fulldoi: https://doi.org/10.1145/3360555
has_accepted_license: '1'
intvolume: '         3'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 267066CE-B435-11E9-9278-68D0E5697425
  name: Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies
- _id: 266EEEC0-B435-11E9-9278-68D0E5697425
  name: Quantitative Game-theoretic Analysis of Blockchain Applications and Smart
    Contracts
publication: 'Proceedings of the 34th ACM International Conference on Object-Oriented
  Programming, Systems, Languages, and Applications '
publication_status: published
publisher: ACM
quality_controlled: '1'
related_material:
  record:
  - id: '8934'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Modular verification for almost-sure termination of probabilistic programs
tmp:
  image: /images/cc_by_nc.png
  legal_code_url: https://creativecommons.org/licenses/by-nc/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)
  short: CC BY-NC (4.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 3
year: '2019'
...