---
res:
  bibo_abstract:
  - '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.@eng'
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - foaf_Person:
      foaf_givenName: Ehsan
      foaf_name: Kafshdar Goharshadi, Ehsan
      foaf_surname: Kafshdar Goharshadi
      foaf_workInfoHomepage: http://www.librecat.org/personId=103b4fa0-896a-11ed-bdf8-87b697bef40d
    orcid: 0000-0002-8595-0587
  - foaf_Person:
      foaf_givenName: Dorde
      foaf_name: Zikelic, Dorde
      foaf_surname: Zikelic
      foaf_workInfoHomepage: http://www.librecat.org/personId=294AA7A6-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4681-1699
  bibo_doi: 10.1145/3808296
  bibo_issue: PLDI
  bibo_volume: 10
  dct_date: 2026^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2475-1421
  dct_language: eng
  dct_publisher: Association for Computing Machinery@
  dct_subject:
  - Static Program Analysis
  - Differential Privacy
  - Probabilistic Programming
  - Martingales
  dct_title: 'SuperDP: Differential privacy refutation via supermartingales@'
...