---
OA_place: publisher
OA_type: gold
PlanS_conform: '1'
_id: '22102'
abstract:
- lang: eng
  text: 'Differential privacy (DP) has established itself as one of the standards
    for ensuring privacy of individual data. However, reasoning about DP is a challenging
    and error-prone task, hence methods for formal verification and refutation of
    DP properties have received significant interest in recent years. In this work,
    we present a novel method for automated formal refutation of є-DP. Our method
    refutes є-DP by searching for a pair of inputs together with a non-negative function
    over outputs whose expected value on these two inputs differs by a significant
    amount. The two inputs and the non-negative function over outputs are computed
    simultaneously, by utilizing upper expectation supermartingales and lower expectation
    submartingales from probabilistic program analysis, which we leverage to introduce
    a sound and complete proof rule for є-DP refutation. To the best of our knowledge,
    our method is the first method for є-DP refutation to offer the following four
    desirable features: (1) it is fully automated, (2) it is applicable to stochastic
    mechanisms with sampling instructions from both discrete and continuous distributions,
    (3) it provides soundness guarantees, and (4) it provides semi-completeness guarantees.
    Our experiments show that our prototype tool SuperDP achieves superior performance
    compared to the state of the art and manages to refute є-DP for a number of challenging
    examples collected from the literature, including ones that were out of the reach
    of prior methods.'
acknowledgement: "The authors would like to thank Petr Novotný for valuable discussions
  that helped shape this work.\r\nThis research was supported by the Singapore Ministry
  of Education (MOE) Academic Research\r\nFund (AcRF) Tier 1 grant (Proposal ID: 25-SIS-SMU-009),
  Vienna Science and Technology Fund\r\n(WWTF), State of Lower Austria [Grant ID 10.47379/ICT25017],
  ERC CoG 863818 (ForM-SMArt),\r\nand Austrian Science Fund (FWF) 10.55776/COE12."
article_number: '218'
article_processing_charge: Yes
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Ehsan
  full_name: Kafshdar Goharshadi, Ehsan
  id: 103b4fa0-896a-11ed-bdf8-87b697bef40d
  last_name: Kafshdar Goharshadi
  orcid: 0000-0002-8595-0587
- first_name: Dorde
  full_name: Zikelic, Dorde
  id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
  last_name: Zikelic
  orcid: 0000-0002-4681-1699
citation:
  ama: 'Chatterjee K, Goharshady E, Zikelic D. SuperDP: Differential privacy refutation
    via supermartingales. <i>Proceedings of the ACM on Programming Languages</i>.
    2026;10(PLDI). doi:<a href="https://doi.org/10.1145/3808296">10.1145/3808296</a>'
  apa: 'Chatterjee, K., Goharshady, E., &#38; Zikelic, D. (2026). SuperDP: Differential
    privacy refutation via supermartingales. <i>Proceedings of the ACM on Programming
    Languages</i>. Association for Computing Machinery. <a href="https://doi.org/10.1145/3808296">https://doi.org/10.1145/3808296</a>'
  chicago: 'Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP:
    Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM
    on Programming Languages</i>. Association for Computing Machinery, 2026. <a href="https://doi.org/10.1145/3808296">https://doi.org/10.1145/3808296</a>.'
  ieee: 'K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential privacy
    refutation via supermartingales,” <i>Proceedings of the ACM on Programming Languages</i>,
    vol. 10, no. PLDI. Association for Computing Machinery, 2026.'
  ista: 'Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy
    refutation via supermartingales. Proceedings of the ACM on Programming Languages.
    10(PLDI), 218.'
  mla: 'Chatterjee, Krishnendu, et al. “SuperDP: Differential Privacy Refutation via
    Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>, vol.
    10, no. PLDI, 218, Association for Computing Machinery, 2026, doi:<a href="https://doi.org/10.1145/3808296">10.1145/3808296</a>.'
  short: K. Chatterjee, E. Goharshady, D. Zikelic, Proceedings of the ACM on Programming
    Languages 10 (2026).
corr_author: '1'
das_tickbox: '1'
dataavailabilitystatement: "The artifact supporting the findings of this study, which
  includes the underlying datasets, software\r\ncode, and experiments, is publicly
  available in Zenodo https://zenodo.org/records/19399862."
date_created: 2026-06-21T22:02:59Z
date_published: 2026-06-08T00:00:00Z
date_updated: 2026-06-24T06:39:37Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3808296
ec_funded: 1
external_id:
  arxiv:
  - '2603.26215'
file:
- access_level: open_access
  checksum: 994bf21d6269dabccf1e1091e02962c5
  content_type: application/pdf
  creator: dernst
  date_created: 2026-06-24T06:19:56Z
  date_updated: 2026-06-24T06:19:56Z
  file_id: '22135'
  file_name: 2026_ProcACMProgrammingLanguages_Chatterjee.pdf
  file_size: 858595
  relation: main_file
  success: 1
file_date_updated: 2026-06-24T06:19:56Z
has_accepted_license: '1'
intvolume: '        10'
issue: PLDI
keyword:
- Static Program Analysis
- Differential Privacy
- Probabilistic Programming
- Martingales
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
  eissn:
  - 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '22134'
    relation: research_data
    status: public
researchdata_availability: yes
scopus_import: '1'
status: public
supplementarymaterial: no
title: 'SuperDP: Differential privacy refutation via supermartingales'
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10
year: '2026'
...
---
_id: '6175'
abstract:
- lang: eng
  text: "We consider the problem of expected cost analysis over nondeterministic probabilistic
    programs,\r\nwhich aims at automated methods for analyzing the resource-usage
    of such programs.\r\nPrevious approaches for this problem could only handle nonnegative
    bounded costs.\r\nHowever, in many scenarios, such as queuing networks or analysis
    of cryptocurrency protocols,\r\nboth positive and negative costs are necessary
    and the costs are unbounded as well.\r\n\r\nIn this work, we present a sound and
    efficient approach to obtain polynomial bounds on the\r\nexpected accumulated
    cost of nondeterministic probabilistic programs.\r\nOur approach can handle (a)
    general positive and negative costs with bounded updates in\r\nvariables; and
    (b) nonnegative costs with general updates to variables.\r\nWe show that several
    natural examples which could not be\r\nhandled by previous approaches are captured
    in our framework.\r\n\r\nMoreover, our approach leads to an efficient polynomial-time
    algorithm, while no\r\nprevious approach for cost analysis of probabilistic programs
    could guarantee polynomial runtime.\r\nFinally, we show the effectiveness of our
    approach using experimental results on a variety of programs for which we efficiently
    synthesize tight resource-usage bounds."
article_processing_charge: No
arxiv: 1
author:
- first_name: Peixin
  full_name: Wang, Peixin
  last_name: Wang
- first_name: Hongfei
  full_name: Fu, Hongfei
  id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
  last_name: Fu
- first_name: Amir Kafshdar
  full_name: Goharshady, Amir Kafshdar
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Xudong
  full_name: Qin, Xudong
  last_name: Qin
- first_name: Wenjun
  full_name: Shi, Wenjun
  last_name: Shi
citation:
  ama: 'Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. Cost analysis of
    nondeterministic probabilistic programs. In: <i>PLDI 2019: Proceedings of the
    40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>.
    Association for Computing Machinery; 2019:204-220. doi:<a href="https://doi.org/10.1145/3314221.3314581">10.1145/3314221.3314581</a>'
  apa: 'Wang, P., Fu, H., Goharshady, A. K., Chatterjee, K., Qin, X., &#38; Shi, W.
    (2019). Cost analysis of nondeterministic probabilistic programs. In <i>PLDI 2019:
    Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design
    and Implementation</i> (pp. 204–220). Phoenix, AZ, United States: Association
    for Computing Machinery. <a href="https://doi.org/10.1145/3314221.3314581">https://doi.org/10.1145/3314221.3314581</a>'
  chicago: 'Wang, Peixin, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee,
    Xudong Qin, and Wenjun Shi. “Cost Analysis of Nondeterministic Probabilistic Programs.”
    In <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming
    Language Design and Implementation</i>, 204–20. Association for Computing Machinery,
    2019. <a href="https://doi.org/10.1145/3314221.3314581">https://doi.org/10.1145/3314221.3314581</a>.'
  ieee: 'P. Wang, H. Fu, A. K. Goharshady, K. Chatterjee, X. Qin, and W. Shi, “Cost
    analysis of nondeterministic probabilistic programs,” in <i>PLDI 2019: Proceedings
    of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>,
    Phoenix, AZ, United States, 2019, pp. 204–220.'
  ista: 'Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. 2019. Cost analysis
    of nondeterministic probabilistic programs. PLDI 2019: Proceedings of the 40th
    ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI:
    Conference on Programming Language Design and Implementation, 204–220.'
  mla: 'Wang, Peixin, et al. “Cost Analysis of Nondeterministic Probabilistic Programs.”
    <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language
    Design and Implementation</i>, Association for Computing Machinery, 2019, pp.
    204–20, doi:<a href="https://doi.org/10.1145/3314221.3314581">10.1145/3314221.3314581</a>.'
  short: 'P. Wang, H. Fu, A.K. Goharshady, K. Chatterjee, X. Qin, W. Shi, in:, PLDI
    2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design
    and Implementation, Association for Computing Machinery, 2019, pp. 204–220.'
conference:
  end_date: 2019-06-26
  location: Phoenix, AZ, United States
  name: 'PLDI: Conference on Programming Language Design and Implementation'
  start_date: 2019-06-22
date_created: 2019-03-25T10:13:25Z
date_published: 2019-06-08T00:00:00Z
date_updated: 2026-06-27T22:31:08Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3314221.3314581
ec_funded: 1
external_id:
  arxiv:
  - '1902.04659'
  isi:
  - '000523190300014'
file:
- access_level: open_access
  checksum: 703a5e9b8c8587f2a44085ffd9a4db64
  content_type: application/pdf
  creator: akafshda
  date_created: 2019-03-25T10:11:22Z
  date_updated: 2020-07-14T12:47:20Z
  file_id: '6176'
  file_name: paper.pdf
  file_size: 4051066
  relation: main_file
file_date_updated: 2020-07-14T12:47:20Z
has_accepted_license: '1'
isi: 1
keyword:
- Program Cost Analysis
- Program Termination
- Probabilistic Programs
- Martingales
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 204-220
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: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 266EEEC0-B435-11E9-9278-68D0E5697425
  name: Quantitative Game-theoretic Analysis of Blockchain Applications and Smart
    Contracts
publication: 'PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming
  Language Design and Implementation'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '5457'
    relation: earlier_version
    status: public
  - id: '8934'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Cost analysis of nondeterministic probabilistic programs
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2019'
...