pith. sign in

arxiv: 2603.26215 · v2 · submitted 2026-03-27 · 💻 cs.PL · cs.FL· cs.LO

SuperDP: Differential Privacy Refutation via Supermartingales

Krishnendu Chatterjee , Ehsan Kafshdar Goharshady , {\DJ}or{\dj}e \v{Z}ikeli\'c This is my paper

Pith reviewed 2026-05-14 22:55 UTC · model grok-4.3

classification 💻 cs.PL cs.FLcs.LO
keywords differential privacyrefutationsupermartingalesprobabilistic programsautomated verificationstochastic mechanismssoundnesssemi-completeness
0
0 comments X

The pith

A supermartingale-based proof rule enables the first fully automated refutation of ε-differential privacy for stochastic programs with discrete or continuous sampling.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a method called SuperDP that refutes ε-differential privacy by searching for input pairs and non-negative output functions whose expectations differ by more than the allowed ε factor. It simultaneously computes these witnesses using upper-expectation supermartingales and lower-expectation submartingales drawn from probabilistic program analysis. This yields a sound and semi-complete proof rule that applies to programs containing sampling from both discrete and continuous distributions. The approach is fully automated and has been implemented in a prototype that refutes privacy claims on examples previously unreachable by other tools. A reader would care because manual DP reasoning is error-prone and existing automated methods lacked the combination of automation, broad applicability, and formal guarantees.

Core claim

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: it is fully automated, it is applicable to stochastic mechanisms with sampling instructions from

What carries the argument

Upper expectation supermartingales and lower expectation submartingales, which act as witnesses that bound the difference in expected values between two chosen inputs and thereby certify a violation of the ε-DP definition.

If this is right

  • Privacy engineers gain an automated checker that can disprove ε-DP claims for programs with both discrete and continuous random draws.
  • Any refutation produced by the method is guaranteed to be correct because of the underlying soundness argument.
  • When a violation exists and the supermartingale search terminates, a witness pair and function are guaranteed to be found.
  • The same machinery can be applied to programs that prior automated refutation tools could not handle.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The supermartingale technique may generalize to automated refutation of other probabilistic properties such as (ε,δ)-DP or concentrated DP.
  • Integration into existing probabilistic program verifiers could allow routine privacy auditing during development.
  • The semi-completeness result suggests that termination heuristics or ranking functions could turn the method into a practical decision procedure for many programs.
  • Similar expectation-based witnesses might be synthesized for refuting properties in continuous-state Markov decision processes.

Load-bearing premise

Supermartingales and submartingales can be automatically synthesized to witness refutations and the search procedure terminates with a valid witness whenever a violation exists.

What would settle it

A program that violates ε-DP for which the synthesis procedure returns no supermartingale witness or fails to terminate despite the existence of a violation.

Figures

Figures reproduced from arXiv: 2603.26215 by {\DJ}or{\dj}e \v{Z}ikeli\'c, Ehsan Kafshdar Goharshady, Krishnendu Chatterjee.

Figure 1
Figure 1. Figure 1: Our two running examples for illustrating our approach to refuting [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Details of RR-2 and PrivBernoulli benchmarks of Section 6 Input : 𝑥 ∈ [0, 1] Sim : 𝑜𝑢𝑡 1 = 𝑜𝑢𝑡 2 = 0 ∧ |𝑥 1 − 𝑥 2 | ≤ 1 𝑙1: if 𝑥 ==1: 𝑙2: if prob (1 − 10−6): 𝑙3: 𝑜𝑢𝑡 := 0 else : 𝑙4: 𝑜𝑢𝑡 := 0 else : 𝑙5: 𝑜𝑢𝑡 := 0 𝑙𝑡 : Output : 𝑜𝑢𝑡 (a) The lowprob benchmark. Provides no DP guarantees. Creates a delusion of full differential privacy (0-DP) by almost always returning 0. Input : 𝑞 ∈ Z Sim : 𝑜𝑢𝑡 1 = 𝑜𝑢𝑡 2 = 0 ∧ |… view at source ↗
Figure 3
Figure 3. Figure 3: Details of lowprob and geometric benchmarks of Section 6 G Other Related Works G.1 Verification of DP Formal methods for verification of differential privacy have been studied since its introduction in the seminal papers of Dwork et al. [33, 34]. Several works considered questions related to the computational complexity of verifying DP for various classes of programs, e.g. programs with boolean variables [… view at source ↗
read the original 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 $\epsilon$-DP. Our method refutes $\epsilon$-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 $\epsilon$-DP refutation. To the best of our knowledge, our method is the first method for $\epsilon$-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 $\epsilon$-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The manuscript presents SuperDP, a method for automated refutation of ε-differential privacy. It simultaneously synthesizes a pair of inputs and a non-negative function over outputs (witnessed via upper-expectation supermartingales and lower-expectation submartingales drawn from probabilistic program analysis) to demonstrate a violation. The central contribution is a sound and semi-complete proof rule that is claimed to be fully automated and applicable to stochastic mechanisms involving both discrete and continuous sampling distributions, with experiments showing it refutes DP for challenging literature examples beyond the reach of prior tools.

Significance. If the soundness and semi-completeness claims hold (including for continuous distributions), the work would be significant as the first automated DP refutation technique combining full automation, broad applicability to discrete/continuous sampling, and formal guarantees. It builds directly on established supermartingale techniques from probabilistic program analysis and demonstrates practical utility on literature benchmarks, potentially enabling refutation of more complex mechanisms than existing methods.

major comments (3)
  1. [§3] §3 (proof rule): The abstract states both a 'sound and complete proof rule' and 'semi-completeness guarantees'; the precise statement of what is proven (soundness of the rule vs. semi-completeness of the overall procedure) must be clarified with an explicit theorem statement, as semi-completeness appears to depend on the synthesis procedure rather than the rule alone.
  2. [§4] §4 (synthesis algorithm): Semi-completeness for continuous distributions is asserted but not established; the description of template shapes, constraint generation, and enumeration strategy lacks a termination or completeness argument showing that a witness supermartingale/submartingale will be found whenever an ε-DP violation exists. Without this, the four-feature claim (fully automated + semi-complete for continuous sampling) does not hold.
  3. [§5.3] §5.3 (experimental evaluation): The claim that certain examples 'were out of the reach of prior methods' is not supported by direct comparison data; the table or figure reporting runtimes and refutation results should include the specific prior tools attempted on each benchmark and their failure modes to substantiate superiority.
minor comments (2)
  1. [§2] Notation for upper/lower expectations and the distinction between supermartingales and submartingales should be introduced with a small illustrative example in the preliminaries section to aid readability.
  2. The manuscript would benefit from an explicit statement of the limitations of the current synthesis templates (e.g., polynomial degree bounds) even if they do not affect the central claims.

Simulated Author's Rebuttal

3 responses · 0 unresolved

Thank you for the referee's thoughtful review and valuable suggestions. We appreciate the opportunity to clarify and strengthen our manuscript. Below we provide point-by-point responses to the major comments.

read point-by-point responses

  1. Referee: [§3] §3 (proof rule): The abstract states both a 'sound and complete proof rule' and 'semi-completeness guarantees'; the precise statement of what is proven (soundness of the rule vs. semi-completeness of the overall procedure) must be clarified with an explicit theorem statement, as semi-completeness appears to depend on the synthesis procedure rather than the rule alone.

    Authors: We agree that the abstract's wording is ambiguous and could lead to confusion. The proof rule in Section 3 is sound and complete in the sense that if a suitable supermartingale/submartingale witness exists, the rule correctly refutes ε-DP. The semi-completeness is a property of the synthesis algorithm that searches for such witnesses. We will revise the abstract to use consistent terminology ('sound proof rule with semi-completeness guarantees for the synthesis procedure') and include an explicit theorem statement in Section 3 that separates the soundness of the rule from the semi-completeness of the procedure. revision: yes

  2. Referee: [§4] §4 (synthesis algorithm): Semi-completeness for continuous distributions is asserted but not established; the description of template shapes, constraint generation, and enumeration strategy lacks a termination or completeness argument showing that a witness supermartingale/submartingale will be found whenever an ε-DP violation exists. Without this, the four-feature claim (fully automated + semi-complete for continuous sampling) does not hold.

    Authors: The referee is correct that a formal argument for semi-completeness in the continuous case is not fully detailed in the manuscript. The synthesis relies on enumerating a finite set of template shapes for the supermartingales, which is designed to be complete for a broad class of mechanisms but lacks an explicit proof of termination or that it will always find a witness if one exists (noting that the general problem is undecidable). We will add a subsection discussing the semi-completeness conditions, including why the template enumeration provides semi-completeness for the considered benchmarks and literature examples, while acknowledging limitations for arbitrary continuous distributions. This will support the four-feature claim under the stated assumptions. revision: partial

  3. Referee: [§5.3] §5.3 (experimental evaluation): The claim that certain examples 'were out of the reach of prior methods' is not supported by direct comparison data; the table or figure reporting runtimes and refutation results should include the specific prior tools attempted on each benchmark and their failure modes to substantiate superiority.

    Authors: We concur that providing direct comparison data would better substantiate our claims of superiority. We will expand the experimental evaluation in Section 5.3 to include a detailed table listing each benchmark, the prior tools (such as those from related work) that were attempted, their specific failure modes (e.g., timeout, inability to handle continuous distributions, or failure to find a refutation), and the runtimes for SuperDP. This will clearly demonstrate which examples were beyond the reach of prior methods. revision: yes

Circularity Check

0 steps flagged

Derivation applies established supermartingale theory without self-referential reduction

full rationale

The paper develops a new proof rule for ε-DP refutation by leveraging upper-expectation supermartingales and lower-expectation submartingales drawn from prior probabilistic program analysis. Soundness follows directly from the martingale properties (non-negative functions whose expectations decrease or increase in a controlled way), and semi-completeness is stated to follow from the existence of such witnesses when a violation occurs. No equation in the provided description defines the supermartingales in terms of the DP refutation result itself, nor renames a fitted parameter as a prediction, nor reduces the central claim to a self-citation chain whose verification depends on the present work. The synthesis procedure is presented as a practical search enabled by the rule rather than a definitional loop. The derivation therefore remains self-contained against external benchmarks in martingale theory.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the soundness of a new proof rule that reduces ε-DP refutation to the existence of supermartingales witnessing expectation differences; it draws on standard probability theory and the definition of differential privacy.

axioms (2)
  • standard math Standard properties of upper and lower expectations and supermartingales in probabilistic programs
    Invoked to establish the sound and complete proof rule for refutation.
  • domain assumption The standard definition of ε-differential privacy as a bound on output distribution ratios
    The target property being refuted by the synthesized witnesses.

pith-pipeline@v0.9.0 · 5580 in / 1360 out tokens · 48267 ms · 2026-05-14T22:55:58.182345+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

77 extracted references · 77 canonical work pages

  1. [1]

    Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. 2021. Learning Probabilistic Termination Proofs. InComputer Aided Verification - 33rd International Conference, CA V 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II (Lecture 22 Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, and Ðorđe Źikelić Notes in Computer Science, Vol. 12760), Alexandr...

    work page doi:10.1007/978- 2021

  2. [2]

    Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. 2024. Stochastic Omega-Regular Verification and Control with Supermartingales. InCA V (3) (Lecture Notes in Computer Science, Vol. 14683). Springer, 395–419. doi:10.1007/978-3-031- 65633-0_18

    work page doi:10.1007/978-3-031- 2024

  3. [3]

    Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. 2025. Quantitative Supermartingale Certificates. InComputer Aided Verification - 37th International Conference, CA V 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part II. 3–28. doi:10.1007/978-3-031-98679-6_1

    work page doi:10.1007/978-3-031-98679-6_1 2025

  4. [4]

    Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. 2018. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs.Proc. ACM Program. Lang.2, POPL (2018). doi:10.1145/ 3158122

    work page 2018

  5. [5]

    Ali Asadi, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. 2021. Polynomial reachability witnesses via Stellensätze. InPLDI. ACM, 772–787. doi:10.1145/3453483.3454076

    work page doi:10.1145/3453483.3454076 2021

  6. [6]

    Martin Avanzini, Gilles Barthe, Davide Davoli, and Benjamin Grégoire. 2025. A Quantitative Probabilistic Relational Hoare Logic.Proc. ACM Program. Lang.9, POPL (2025), 1167–1195. doi:10.1145/3704876

    work page doi:10.1145/3704876 2025

  7. [7]

    equality

    Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, and Mahesh Viswanathan. 2020. Deciding Differential Privacy for Programs with Finite Inputs and Outputs. InLICS. ACM, 141–154. doi:10.1145/3373718.3394796

    work page doi:10.1145/3373718.3394796 2020

  8. [8]

    Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub. 2014. Proving Differential Privacy in Hoare Logic. InCSF. IEEE Computer Society, 411–424. doi:10.1109/CSF.2014.36

    work page doi:10.1109/csf.2014.36 2014

  9. [9]

    Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. Proving Differential Privacy via Probabilistic Couplings. InLICS. ACM, 749–758. doi:10.1145/2933575.2934554

    work page doi:10.1145/2933575.2934554 2016

  10. [10]

    Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. 2009. Formal certification of code-based cryptographic proofs. InPOPL. ACM, 90–101. doi:10.1145/1480881.1480894

    work page doi:10.1145/1480881.1480894 2009

  11. [11]

    Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin. 2013. Probabilistic Relational Reasoning for Differential Privacy.ACM Trans. Program. Lang. Syst.35, 3 (2013), 9:1–9:49. doi:10.1145/2492061

    work page doi:10.1145/2492061 2013

  12. [12]

    Benjamin Bichsel, Timon Gehr, Dana Drachsler-Cohen, Petar Tsankov, and Martin T. Vechev. 2018. DP-Finder: Finding Differential Privacy Violations by Sampling and Optimization. InCCS. ACM, 508–524. doi:10.1145/3243734.3243863

    work page doi:10.1145/3243734.3243863 2018

  13. [13]

    Benjamin Bichsel, Samuel Steffen, Ilija Bogunovic, and Martin T. Vechev. 2021. DP-Sniper: Black-Box Discovery of Differential Privacy Violations using Classifiers. InSP. IEEE, 391–409. doi:10.1109/SP40001.2021.00081

    work page doi:10.1109/sp40001.2021.00081 2021

  14. [14]

    Andrea Bittau, Úlfar Erlingsson, Petros Maniatis, Ilya Mironov, Ananth Raghunathan, David Lie, Mitch Rudominer, Ushasree Kode, Julien Tinnés, and Bernhard Seefeld. 2017. Prochlo: Strong Privacy for Analytics in the Crowd. In Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, October 28-31, 2017. ACM, 441–459. doi:10.1145/3...

    work page doi:10.1145/3132747.3132769 2017

  15. [15]

    Mark Bun, Marco Gaboardi, and Ludmila Glinskih. 2022. The Complexity of Verifying Boolean Programs as Differentially Private. InCSF. IEEE, 396–411. doi:10.1109/CSF54842.2022.9919653

    work page doi:10.1109/csf54842.2022.9919653 2022

  16. [16]

    Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. InCA V (Lecture Notes in Computer Science, Vol. 8044). Springer, 511–526. doi:10.1007/978-3-642-39799-8_34

    work page doi:10.1007/978-3-642-39799-8_34 2013

  17. [17]

    Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz’s. InCA V (1) (Lecture Notes in Computer Science, Vol. 9779). Springer, 3–22. doi:10.1007/978-3-319-41528-4_1

    work page doi:10.1007/978-3-319-41528-4_1 2016

  18. [18]

    Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. 2020. Polynomial invariant generation for non-deterministic recursive programs(PLDI 2020). doi:10.1145/3385412.3385969

    work page doi:10.1145/3385412.3385969 2020

  19. [19]

    Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. 2018. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.ACM Trans. Program. Lang. Syst.40, 2 (2018). doi:10.1145/3174800

    work page doi:10.1145/3174800 2018

  20. [20]

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. 2022. Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs. InComputer Aided Verification - 34th International Conference, CA V 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I (Lecture Notes in Computer Science, V...

    work page doi:10.1007/978-3-031-13185-1_4 2022

  21. [21]

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. 2024. Quantitative Bounds on Resource Usage of Probabilistic Programs.Proc. ACM Program. Lang.8, OOPSLA1 (2024), 362–391. doi:10.1145/3649824

    work page doi:10.1145/3649824 2024

  22. [22]

    Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiri Zárevúcky, and Dorde Zikelic. 2023. On Lexicographic Proof Rules for Probabilistic Termination.Formal Aspects Comput.35, 2 (2023), 11:1–11:25. doi:10.1145/ 3585391

    work page 2023

  23. [23]

    Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. 2024. Equivalence and Similarity Refutation for Probabilistic Programs.Proc. ACM Program. Lang.8, PLDI (2024), 2098–2122. doi:10.1145/3656462 SuperDP: Differential Privacy Refutation via Supermartingales 23

    work page doi:10.1145/3656462 2024

  24. [24]

    Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. 2025. Refuting Equivalence in Probabilistic Programs with Conditioning. InTACAS (2) (Lecture Notes in Computer Science, Vol. 15697). Springer, 279–300. doi:10.1007/978-3-031-90653-4_14

    work page doi:10.1007/978-3-031-90653-4_14 2025

  25. [25]

    Krishnendu Chatterjee, Petr Novotný, and Dorde Zikelic. 2017. Stochastic invariants for probabilistic termination. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 145–160. doi:10.1145/3009837.3009873

    work page doi:10.1145/3009837.3009873 2017

  26. [26]

    Jianhui Chen and Fei He. 2020. Proving almost-sure termination by omega-regular decomposition. InProceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 869–882. doi:10.1145/3385412.3386002

    work page doi:10.1145/3385412.3386002 2020

  27. [27]

    Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. 2013. The MathSAT5 SMT Solver. InTools and Algorithms for the Construction and Analysis of Systems. doi:10.1007/978-3-642-36742-7_7

    work page doi:10.1007/978-3-642-36742-7_7 2013

  28. [28]

    Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. InComputer Aided Verification, 15th International Conference, CA V 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2725), Warren A. Hunt Jr. and Fabio Somenzi (Eds.). Springer, 420–43...

    work page doi:10.1007/978-3-540-45069-6_39 2003

  29. [29]

    Michael Colón and Henny Sipma. 2001. Synthesis of Linear Ranking Functions. InTools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings (Lecture Notes in Computer Scienc...

    work page doi:10.1007/3-540-45319-9_6 2001

  30. [30]

    Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: an efficient SMT solver. InProceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08). doi:10.1007/978-3-540-78800-3_24

    work page doi:10.1007/978-3-540-78800-3_24 2008

  31. [31]

    Bolin Ding, Janardhan Kulkarni, and Sergey Yekhanin. 2017. Collecting Telemetry Data Privately. InAdvances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanatha...

    work page 2017

  32. [32]

    Zeyu Ding, Yuxin Wang, Guanhong Wang, Danfeng Zhang, and Daniel Kifer. 2018. Detecting Violations of Differential Privacy. InCCS. ACM, 475–489. doi:10.1145/3243734.3243818

    work page doi:10.1145/3243734.3243818 2018

  33. [33]

    Cynthia Dwork. 2006. Differential Privacy. InAutomata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 4052), Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener (Eds.). Springer, 1–12. doi:10.1007/11787006_1

    work page doi:10.1007/11787006_1 2006

  34. [34]

    Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam D. Smith. 2006. Calibrating Noise to Sensitivity in Private Data Analysis. InTCC (Lecture Notes in Computer Science). Springer. doi:10.29012/JPC.V7I3.405

    work page doi:10.29012/jpc.v7i3.405 2006

  35. [35]

    Proceedings of the Forty-First Annual ACM Symposium on Theory of Computing , pages =

    Cynthia Dwork, Moni Naor, Omer Reingold, Guy N. Rothblum, and Salil P. Vadhan. 2009. On the complexity of differentially private data release: efficient algorithms and hardness results. InProceedings of the 41st Annual ACM Symposium on Theory of Computing, STOC 2009, Bethesda, MD, USA, May 31 - June 2, 2009, Michael Mitzenmacher (Ed.). ACM, 381–390. doi:1...

    work page doi:10.1145/1536414.1536467 2009

  36. [36]

    Cynthia Dwork and Aaron Roth. 2014. The Algorithmic Foundations of Differential Privacy.Found. Trends Theor. Comput. Sci.9, 3-4 (2014), 211–407. doi:10.1561/0400000042

    work page doi:10.1561/0400000042 2014

  37. [37]

    Gian Pietro Farina, Stephen Chong, and Marco Gaboardi. 2021. Coupled Relational Symbolic Execution for Differential Privacy. InESOP (Lecture Notes in Computer Science, Vol. 12648). Springer, 207–233. doi:10.1007/978-3-030-72019-3_8

    work page doi:10.1007/978-3-030-72019-3_8 2021

  38. [38]

    Paul Feautrier and Laure Gonnord. [n. d.]. Accelerated Invariant Generation for C Programs with Aspic and C2fsm. Electronic Notes in Theoretical Computer Science([n. d.]). doi:10.1016/j.entcs.2010.09.014

    work page doi:10.1016/j.entcs.2010.09.014 2010

  39. [39]

    Marco Gaboardi, Kobbi Nissim, and David Purser. 2020. The Complexity of Verifying Loop-Free Programs as Differentially Private. InICALP (LIPIcs, Vol. 168). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 129:1–129:17. doi:10.4230/LIPICS.ICALP.2020.129

    work page doi:10.4230/lipics.icalp.2020.129 2020

  40. [40]

    Timon Gehr, Sasa Misailovic, and Martin T. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In CA V (1) (Lecture Notes in Computer Science, Vol. 9779). Springer, 62–83. doi:10.1007/978-3-319-41528-4_4

    work page doi:10.1007/978-3-319-41528-4_4 2016

  41. [41]

    Quan Geng and Pramod Viswanath. 2016. The Optimal Noise-Adding Mechanism in Differential Privacy.IEEE Trans. Inf. Theory62, 2 (2016), 925–951. doi:10.1109/TIT.2015.2504967

    work page doi:10.1109/tit.2015.2504967 2016

  42. [42]

    Zoubin Ghahramani. 2015. Probabilistic machine learning and artificial intelligence.Nat.521, 7553 (2015), 452–459. doi:10.1038/NATURE14541

    work page doi:10.1038/nature14541 2015

  43. [43]

    Ji Guan, Wang Fang, Mingyu Huang, and Mingsheng Ying. 2023. Detecting Violations of Differential Privacy for Quantum Algorithms. InCCS. ACM, 2277–2291. doi:10.1145/3576915.3623108

    work page doi:10.1145/3576915.3623108 2023

  44. [44]

    David Handelman. 1988. Representing polynomials by positive linear functions on compact convex polyhedra.Pacific J. Math.132, 1 (1988), 35 – 62. 24 Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, and Ðorđe Źikelić

    work page 1988

  45. [45]

    Henzinger, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic

    Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic. 2025. Supermartingale Certificates for Quantitative Omega-Regular Verification and Control. InComputer Aided Verification - 37th International Conference, CA V 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part II. 29–55. doi:10.1007/978-3-031-98679-6_2

    work page doi:10.1007/978-3-031-98679-6_2 2025

  46. [46]

    Johnson, Joseph P

    Noah M. Johnson, Joseph P. Near, and Dawn Song. 2018. Towards Practical Differential Privacy for SQL Queries.Proc. VLDB Endow.11, 5 (2018), 526–539. doi:10.1145/3187009.3177733

    work page doi:10.1145/3187009.3177733 2018

  47. [47]

    Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms.J. ACM65, 5 (2018), 30:1–30:68. doi:10.1145/3208102

    work page doi:10.1145/3208102 2018

  48. [48]

    Min Lyu, Dong Su, and Ninghui Li. 2017. Understanding the Sparse Vector Technique for Differential Privacy.Proc. VLDB Endow.10, 6 (2017), 637–648. doi:10.14778/3055330.3055331

    work page doi:10.14778/3055330.3055331 2017

  49. [49]

    Rupak Majumdar and V. R. Sathiyanarayana. 2024. Positive Almost-Sure Termination: Complexity and Proof Rules. Proc. ACM Program. Lang.8, POPL (2024), 1089–1117. doi:10.1145/3632879

    work page doi:10.1145/3632879 2024

  50. [50]

    Rupak Majumdar and V. R. Sathiyanarayana. 2025. Sound and Complete Proof Rules for Probabilistic Termination. Proc. ACM Program. Lang.9, POPL (2025), 1871–1902. doi:10.1145/3704899

    work page doi:10.1145/3704899 2025

  51. [51]

    Calvert, and Luca Laurenti

    Frederik Baymler Mathiesen, Simeon C. Calvert, and Luca Laurenti. 2023. Safety Certification for Stochastic Systems via Neural Barrier Functions.IEEE Control. Syst. Lett.7 (2023), 973–978. doi:10.1109/LCSYS.2022.3229865

    work page doi:10.1109/lcsys.2022.3229865 2023

  52. [52]

    Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2018. A new proof rule for almost-sure termination.Proc. ACM Program. Lang.2, POPL (2018), 33:1–33:28. doi:10.1145/3158121

    work page doi:10.1145/3158121 2018

  53. [53]

    2012.Markov chains and stochastic stability

    Sean P Meyn and Richard L Tweedie. 2012.Markov chains and stochastic stability. Springer Science & Business Media. doi:10.1007/978-1-4471-3267-7

    work page doi:10.1007/978-1-4471-3267-7 2012

  54. [54]

    Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 496–512. doi:10.1145/3192366.3192394

    work page doi:10.1145/3192366.3192394 2018

  55. [55]

    Andreas Podelski and Andrey Rybalchenko. 2004. A Complete Method for the Synthesis of Linear Ranking Functions. InVerification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings (Lecture Notes in Computer Science, Vol. 2937), Bernhard Steffen and Giorgio Levi (Eds.). Spri...

    work page doi:10.1007/978-3-540-24622-0_20 2004

  56. [56]

    Andreas Podelski and Andrey Rybalchenko. 2004. Transition Invariants. In19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. IEEE Computer Society, 32–41. doi:10.1109/LICS.2004. 1319598

    work page doi:10.1109/lics.2004 2004

  57. [57]

    Stephen Prajna, Ali Jadbabaie, and George J. Pappas. 2007. A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates.IEEE Trans. Autom. Control.52, 8 (2007), 1415–1428. doi:10.1109/TAC.2007.902736

    work page doi:10.1109/tac.2007.902736 2007

  58. [58]

    Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. 2021. Ranking and Repulsing Supermartingales for Reachability in Randomized Programs.ACM Trans. Program. Lang. Syst.43, 2 (2021), 5:1–5:46. doi:10.1145/3450967

    work page doi:10.1145/3450967 2021

  59. [59]

    The OpenDP Team. 2021. The OpenDP Library. https://opendp.org

    work page 2021

  60. [60]

    2024.The Coq Proof Assistant

    The Coq Development Team. 2024.The Coq Proof Assistant. doi:10.5281/zenodo.14542673

    work page doi:10.5281/zenodo.14542673 2024

  61. [61]

    Jan-Willem van de Meent, Brooks Paige, Hongseok Yang, and Frank Wood. 2018. An Introduction to Probabilistic Programming.CoRRabs/1809.10756 (2018). arXiv:1809.10756 http://arxiv.org/abs/1809.10756

    work page arXiv 2018

  62. [62]

    Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu. 2020. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time.Proc. ACM Program. Lang.4, POPL (2020), 25:1–25:30. doi:10.1145/3371093

    work page doi:10.1145/3371093 2020

  63. [63]

    Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. 2019. Cost analysis of nondeterministic probabilistic programs. InPLDI. doi:10.1145/3314221.3314581

    work page doi:10.1145/3314221.3314581 2019

  64. [64]

    Luke Ong

    Peixin Wang, Tengshun Yang, Hongfei Fu, Guanyan Li, and C.-H. Luke Ong. 2024. Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving.Proc. ACM Program. Lang.8, PLDI (2024), 1361–1386. doi:10.1145/3656432

    work page doi:10.1145/3656432 2024

  65. [65]

    Yuxin Wang, Zeyu Ding, Daniel Kifer, and Danfeng Zhang. 2020. CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples. InCCS. ACM, 919–938. doi:10.1145/3372297.3417282

    work page doi:10.1145/3372297.3417282 2020

  66. [66]

    Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, and Danfeng Zhang. 2019. Proving differential privacy with shadow execution. InPLDI. ACM, 655–669. doi:10.1145/3314221.3314619

    work page doi:10.1145/3314221.3314619 2019

  67. [67]

    1991.Probability with Martingales

    David Williams. 1991.Probability with Martingales. Cambridge University Press

    work page 1991

  68. [68]

    Bai Xue. 2025. Finite-time safety and reach-avoid verification of stochastic discrete-time systems.Information and Computation307 (2025), 105368. doi:10.1016/j.ic.2025.105368

    work page doi:10.1016/j.ic.2025.105368 2025

  69. [69]

    Bai Xue. 2026. Sufficient and necessary barrier-like conditions for safety and reach-avoid verification of stochastic discrete-time systems.Automatica187 (2026), 112919. doi:10.1016/j.automatica.2026.112919

    work page doi:10.1016/j.automatica.2026.112919 2026

  70. [70]

    Bai Xue, Renjue Li, Naijun Zhan, and Martin Fränzle. 2021. Reach-avoid Analysis for Stochastic Discrete-time Systems. In2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021. IEEE, 4879–4885. SuperDP: Differential Privacy Refutation via Supermartingales 25 doi:10.23919/ACC50511.2021.9483095

    work page doi:10.23919/acc50511.2021.9483095 2021

  71. [71]

    Danfeng Zhang and Daniel Kifer. 2017. LightDP: towards automating differential privacy proofs. InPOPL. ACM, 888–901. doi:10.1145/3009837.3009884

    work page doi:10.1145/3009837.3009884 2017

  72. [72]

    Luke Ong, and Min Zhang

    Dapeng Zhi, Peixin Wang, Si Liu, C.-H. Luke Ong, and Min Zhang. 2024. Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems. InComputer Aided Verification - 36th International Conference, CA V 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 14682), Arie Gurfinkel and...

    work page doi:10.1007/978-3-031-65630-9_20 2024

  73. [73]

    Dorde Zikelic, Bor-Yuh Evan Chang, Pauline Bolignano, and Franco Raimondi. 2022. Differential cost analysis with simultaneous potentials and anti-potentials. InPLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, Ranjit Jhala and Isil Dillig (Eds.). ACM, 442–457. doi...

    work page doi:10.1145/3519939.3523435 2022

  74. [74]

    Henzinger, and Krishnendu Chatterjee

    Dorde Zikelic, Mathias Lechner, Thomas A. Henzinger, and Krishnendu Chatterjee. 2023. Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees. InThirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educati...

    work page doi:10.1609/aaai.v37i10.26407 2023

  75. [75]

    Henzinger

    Dorde Zikelic, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A. Henzinger. 2023. Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees. InAdvances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 1...

    work page 2023

  76. [76]

    synchronized

    The following table shows an example of a UESM𝑈 𝑓 and an LESM𝐿 𝑓 for this mechanism (rounded to two decimal places): Label UESM 𝑙1 9458.01+4727.0·𝑞 2 0 𝑙2 0.01+4.01·𝑞 0𝜂+1575.67·𝑞 0𝜂3 +2363.5·𝑞 2 0𝜂2 +1575.67·𝑞 3 0𝜂+2.0· ∗𝜂 2 +393.92·𝜂 4 𝑙𝑡 0 Label LESM 𝑙1 9458.01+4727.0·𝑞 2 0 𝑙2 4.01·𝑞 0𝜂+1575.67·𝑞 0𝜂3 +2363.5·𝑞 2 0𝜂2 +1575.67·𝑞 3 0𝜂+2.0· ∗𝜂 2 +393.92·𝜂 ...

    work page

  77. [77]

    uses a template-based method together with a verify-invalidate loop for finding such alignments and provides automation as well

    work page