pith. sign in

arxiv: 2606.15043 · v3 · pith:SYT2LF5Ynew · submitted 2026-06-13 · 💻 cs.PL

Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams

Daniel Basg\"oze , Kevin Batz , Sebastian Junges , Joost-Pieter Katoen This is my paper

Pith reviewed 2026-06-27 04:38 UTC · model grok-4.3

classification 💻 cs.PL
keywords probabilistic program verificationweakest pre-expectationsdecision diagramsdeductive verificationSMT-based pruningloop unrollingscalability
0
0 comments X

The pith

Typed extended decision diagrams let deductive verification of probabilistic programs scale by orders of magnitude.

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

The paper develops typed extended decision diagrams to represent weakest pre-expectations for loops in probabilistic programs without information loss. These diagrams support direct computation of the expectations, followed by SMT-based pruning to shrink them further and adapted proof rules that operate on the diagrams themselves. The result is that verification routines which previously hit size explosions can now handle substantially larger discrete probabilistic programs.

Core claim

Typed extended decision diagrams (TEDDs) are introduced as a representation for weakest pre-expectations on partially unrolled loops; they are computed directly, pruned via SMT solvers, and used as the domain for lifted proof rules, yielding orders-of-magnitude gains in scalability over prior deductive approaches.

What carries the argument

Typed extended decision diagrams (TEDDs), an extension of binary decision diagrams that encodes typed expressions for quantitative expectations and permits both pruning and rule application without loss of precision.

If this is right

  • Verification succeeds on programs whose loop unrollings produce expectations too large for earlier representations.
  • SMT pruning becomes effective on a much wider range of partially unrolled loops.
  • Existing proof rules for expectations can be reused directly on the diagram representation.
  • Automation covers a broader class of discrete probabilistic programs without manual intervention.

Where Pith is reading between the lines

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

  • The same diagram technique could be tested on quantitative properties beyond expectations, such as variance or tail bounds.
  • TEDDs might serve as an intermediate format for exchanging results between different probabilistic verifiers.
  • If the diagrams remain compact under further unrollings, the method could reduce reliance on loop invariants in some cases.

Load-bearing premise

The size explosion in logical representations of weakest pre-expectations on loops can be avoided by a compact diagram representation that still allows exact SMT pruning and rule lifting.

What would settle it

A set of benchmark programs where the TEDD size after pruning is no smaller than the size of the corresponding explicit or BDD-based representation and verification time shows no improvement.

Figures

Figures reproduced from arXiv: 2606.15043 by Daniel Basg\"oze, Joost-Pieter Katoen, Kevin Batz, Sebastian Junges.

Figure 1
Figure 1. Figure 1: Program 𝐶𝑁 and case expression wpJ𝐶𝑁 K (𝑥) for 𝑁 = 3. 𝐴 [0] > 0 𝐴 [1] > 0 𝐴 [1] > 0 𝑥 1/2 · 𝑥 1/4 · 𝑥 (a) TEDD for 𝑁 = 2. 𝐴 [0] > 0 𝐴 [1] > 0 𝐴 [1] > 0 𝐴 [2] > 0 𝐴 [2] > 0 𝐴 [2] > 0 𝑥 1/2 · 𝑥 1/4 · 𝑥 1/8 · 𝑥 (b) TEDD for 𝑁 = 3 [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: TEDDs representing wpJ𝐶𝑁 K (𝑥) for the program 𝐶𝑁 in Figure 1a. In this paper, we reason about expected outcomes of probabilistic programs. For 𝐶𝑁 above, we are interested in the expected final value of 𝑥 obtained upon termination of 𝐶𝑁 . This expected outcome depends on the initial program state, in particular the value of𝐴, as that value determines the control flow. A bit more formal, we are interested i… view at source ↗
Figure 3
Figure 3. Figure 3: A program with conditioning and two equivalent TEDDs, representing the function mapping initial [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Two EUReal-TEDDs, which are equivalent modulo LA. All variables are of type Nat. This operator satisfies Jop [F] (e1, . . . , e𝑛)K I = JF (e1 (I) , . . . , e𝑛 (I))K I , i.e., applying op [F] to e1, . . . , e𝑛 is equivalent to applying F to the terms selected by e1, . . . , e𝑛 for every I. If F simply applies some function symbol 𝐹 to its arguments, we often write op [𝐹 ] instead of op [F]. Our formalizatio… view at source ↗
Figure 5
Figure 5. Figure 5: Counterexample to canonicity modulo first-order logical equivalence. Let [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Illustration of applying Prune to the TEDD from Figure 4a. Example 8.4. Prune is illustrated in [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Exemplification of wp by applying it to the setting from Example 5.2. 9 Syntactic Weakest Pre-Expectations via TEDDs This section marries the WP calculus from Section 5 with the TEDD-based representation of, e.g., expectations, from Section 7. By careful construction, the integration is rather natural. To facilitate the marriage, we introduce wp, a syntactic variant of wp for loop-free programs that operat… view at source ↗
Figure 8
Figure 8. Figure 8: Performance comparison with Caesar on the complete piecewise affine benchmark suite. from Caesar [85] as well as parameterized benchmarks (where we vary, e.g., 𝑛), inspired by the benchmarks from [24, 85]. The details of the benchmarks are given in Appendix D. Performance. In Fig. 8a, we compare the run time of Caesar and DdSolve (single-threaded). On the original benchmarks, Caesar solves instances within… view at source ↗
Figure 9
Figure 9. Figure 9: Scalability comparison with Caesar on two piecewise affine expectations. The benchmarks on top are without arrays, the benchmarks in the bottom row use arrays. 0 100 200 Parameter 0 100 200 300 Time [s] Grid 0 50 100 150 Parameter 0 100 200 300 GeoGrid 0 100 200 Parameter 0 100 200 300 UniformGridWalk 1-thread DDSolve 1-thread Storm 4-thread DDSolve 4-thread Storm 24-thread DDSolve 24-thread Storm [PITH_F… view at source ↗
Figure 10
Figure 10. Figure 10: Scalability comparison with Storm (using ADDs) on three benchmark families. for nonlinear expectations works, yet the cost of some pruning operations is often prohibitive. In fact, like for piecewise affine expectations, the total time by DdSolve is often dominated by a few expensive pruning operations. With non-linear expectations, these operations are handled by an SMT-solver for quantifier-free nonline… view at source ↗
Figure 11
Figure 11. Figure 11: Ablation study (RQ3): The influence of pruning, multithreading, and dedicated data structures. [PITH_FULL_IMAGE:figures/full_fig_p025_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Scalability comparison with Caesar on two more benchmarks that use arrays. 0 10 20 Parameter 0 100 200 300 Time [s] Non. Det. BRP 0 50 100 Parameter 0 100 200 300 Non. Det. GeoGrid 0 100 200 Parameter 0 100 200 300 Non. Det. Grid 1-thread 4-thread 24-thread Caesar [PITH_FULL_IMAGE:figures/full_fig_p037_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Scalability comparison with Caesar on programs utilizing non-determinism. 0 100 200 Parameter 0 100 200 300 Time [s] UniformGridWalk Cond. 0 200 400 Parameter 0 100 200 300 Refute BRP Cond. 0 100 200 Parameter 0 100 200 300 Grid Cond. 1-thread 4-thread 24-thread Caesar [PITH_FULL_IMAGE:figures/full_fig_p037_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Scalability comparison with Caesar on programs utilizing conditioning. C Additional Benchmark Results We present additional benchmark results in [PITH_FULL_IMAGE:figures/full_fig_p037_14.png] view at source ↗
read the original abstract

Weakest pre-expectations are the probabilistic program analogue to weakest preconditions in classical programs. Deductive verification approaches aim to establish bounds on these quantitative expectations. Their automation has been successful in analysing a variety of discrete probabilistic programs. Key routines in that automation require reasoning about (partially unrolled) loops, however, the logical representation of weakest pre-expectations on such unrollings often explodes. In this paper, we develop typed extended decision diagrams (TEDDs), inspired by various extensions to binary decision diagrams. We demonstrate computing WPs represented as TEDDs, SMT-based pruning to further shrink their representation, and we lift some proof rules to operate on TEDDs. Finally, we demonstrate that TEDDs boost the scalability of deductive probabilistic program verification by orders of magnitudes over the state of the art.

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

1 major / 0 minor

Summary. The paper introduces typed extended decision diagrams (TEDDs) as a representation for weakest pre-expectations arising in deductive verification of discrete probabilistic programs. It describes how to compute WPs directly as TEDDs, apply SMT-based pruning to shrink representations, lift selected proof rules to operate on TEDDs, and claims that the resulting pipeline yields orders-of-magnitude scalability gains over prior state-of-the-art methods when reasoning about partially unrolled loops.

Significance. If the claimed scalability improvements are substantiated by concrete evidence, the work would meaningfully advance automated quantitative verification by mitigating the representation-size explosion that currently limits analysis of loops. The combination of typed decision-diagram extensions with SMT pruning and lifted rules constitutes a technically coherent contribution that builds directly on existing BDD and expectation-calculus literature.

major comments (1)
  1. [Abstract] Abstract: the central claim that TEDDs 'boost the scalability ... by orders of magnitudes' is load-bearing for the paper's contribution yet is stated without any quantitative support (no runtimes, no program sizes, no comparison tables). The experimental evaluation must supply concrete measurements (e.g., wall-clock ratios, maximum loop-unrolling depths handled, and baseline comparisons) to make the claim evaluable.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive feedback. We address the major comment on the abstract below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that TEDDs 'boost the scalability ... by orders of magnitudes' is load-bearing for the paper's contribution yet is stated without any quantitative support (no runtimes, no program sizes, no comparison tables). The experimental evaluation must supply concrete measurements (e.g., wall-clock ratios, maximum loop-unrolling depths handled, and baseline comparisons) to make the claim evaluable.

    Authors: We agree that the abstract would benefit from a brief quantitative anchor for the scalability claim. The experimental evaluation in Section 5 already contains the requested concrete measurements, including wall-clock runtimes, program sizes, maximum loop-unrolling depths, and direct comparisons against the prior state-of-the-art on the same benchmarks. In the revised manuscript we will update the abstract to include a short summary sentence referencing these results (e.g., “TEDDs enable verification of loops unrolled up to depth 2^10 where prior representations time out, yielding speed-ups of up to three orders of magnitude”). revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper introduces typed extended decision diagrams (TEDDs) as a new representation for weakest pre-expectations in probabilistic program verification. The abstract and described pipeline (WP computation on partial unrollings, TEDD representation, SMT pruning, lifted proof rules) present a constructive technical development without any equations, fitted parameters, or self-citations that reduce the central claims to their own inputs by definition. No self-definitional steps, fitted-input predictions, or load-bearing self-citation chains are present in the provided material; the scalability claim is an empirical assertion about the new artifact rather than a derivation that collapses to prior fitted values or renamed inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based solely on the abstract, no free parameters, axioms, or invented entities are specified; the contribution is presented as a new representation and algorithmic technique.

pith-pipeline@v0.9.1-grok · 5668 in / 960 out tokens · 25029 ms · 2026-06-27T04:38:37.159265+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

102 extracted references · 47 canonical work pages · 2 internal anchors

  1. [1]

    Step-indexed logical relations for countable nondeterminism and probabilistic choice.Proc

    Alejandro Aguirre and Lars Birkedal. Step-indexed logical relations for countable nondeterminism and probabilistic choice.Proc. ACM Program. Lang., 7(POPL):33–60, 2023. doi: 10.1145/3571195. URL https://doi.org/10.1145/3571195

    work page doi:10.1145/3571195 2023

  2. [2]

    Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal

    Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal. Error credits: Resourceful reasoning about error bounds for higher-order probabilistic programs.Proc. ACM Program. Lang., 8(ICFP):284–316, 2024. doi: 10.1145/3674635. URL https://doi.org/10.1145/ 3674635

    work page doi:10.1145/3674635 2024

  3. [3]

    Constraint-based synthesis of coupling proofs

    Aws Albarghouthi and Justin Hsu. Constraint-based synthesis of coupling proofs. InCA V (1), pages 327–346, 2018. doi: 10.1007/978-3-319-96145-3\_18. URL https://dblp.org/rec/conf/cav/AlbarghouthiH18

    work page doi:10.1007/978-3-319-96145-3 2018

  4. [4]

    Synthesizing coupling proofs of differential privacy.Proc

    Aws Albarghouthi and Justin Hsu. Synthesizing coupling proofs of differential privacy.Proc. ACM Program. Lang., 2 (POPL):58:1–58:30, 2018. doi: 10.1145/3158146. URL https://dblp.org/rec/journals/pacmpl/AlbarghouthiH18

    work page doi:10.1145/3158146 2018

  5. [5]

    Modular runtime complexity analysis of probabilistic while programs.CoRR, abs/1908.11343, 2019

    Martin Avanzini, Michael Schaper, and Georg Moser. Modular runtime complexity analysis of probabilistic while programs.CoRR, abs/1908.11343, 2019. URL https://dblp.org/rec/journals/corr/abs-1908-11343

    arXiv 1908

  6. [6]

    A modular cost analysis for probabilistic programs.Proc

    Martin Avanzini, Georg Moser, and Michael Schaper. A modular cost analysis for probabilistic programs.Proc. ACM Program. Lang., 4(OOPSLA):172:1–172:30, 2020. doi: 10.1145/3428240. URL https://dblp.org/rec/journals/pacmpl/ AvanziniMS20

    work page doi:10.1145/3428240 2020

  7. [7]

    Automated expected value analysis of recursive programs

    Martin Avanzini, Georg Moser, and Michael Schaper. Automated expected value analysis of recursive programs. Proc. ACM Program. Lang., 7(PLDI):1050–1072, 2023. doi: 10.1145/3591263. URL https://dblp.org/rec/journals/pacmpl/ AvanziniMS23

    work page doi:10.1145/3591263 2023

  8. [8]

    Bahar, E.A

    R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. InProceedings of 1993 International Conference on Computer Aided Design (ICCAD), pages 188–191, 1993

    1993

  9. [9]

    MIT Press, 2008

    Christel Baier and Joost-Pieter Katoen.Principles of model checking. MIT Press, 2008

    2008

  10. [10]

    Clarke, Vasiliki Hartonas-Garmhausen, Marta Z

    Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen, Marta Z. Kwiatkowska, and Mark Ryan. Symbolic model checking for probabilistic processes. InICALP, volume 1256 ofLecture Notes in Computer Science, pages 430–440. Springer, 1997

    1997

  11. [11]

    Data-driven invariant learning for probabilistic programs

    Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. Data-driven invariant learning for probabilistic programs. InCA V (1), pages 33–54, 2022. doi: 10.1007/978-3-031-13185-1\_3. URL https://dblp.org/rec/conf/cav/ BaoTPHR22

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

  12. [12]

    Data-driven invariant learning for probabilistic programs (extended abstract)

    Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. Data-driven invariant learning for probabilistic programs (extended abstract). InIJCAI, pages 6415–6419, 2023. doi: 10.24963/ijcai.2023/712. URL https://dblp.org/ rec/conf/ijcai/BaoTPH023

    work page doi:10.24963/ijcai.2023/712 2023

  13. [13]

    Bluebell: An alliance of relational lifting and independence for probabilistic reasoning.Proc

    Jialu Bao, Emanuele D’Osualdo, and Azadeh Farzan. Bluebell: An alliance of relational lifting and independence for probabilistic reasoning.Proc. ACM Program. Lang., 9(POPL):1719–1749, 2025. doi: 10.1145/3704894. URL https://dblp.org/rec/journals/pacmpl/BaoDF25

    work page doi:10.1145/3704894 2025

  14. [14]

    Data-driven invariant learning for probabilistic programs.Formal Methods Syst

    Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. Data-driven invariant learning for probabilistic programs.Formal Methods Syst. Des., 66(2):278–306, 2025. doi: 10.1007/s10703-024-00466-x. URL https://dblp.org/rec/ journals/fmsd/BaoTPHR25

    work page doi:10.1007/s10703-024-00466-x 2025

  15. [15]

    Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. InTACAS (1), volume 13243 of Lecture Notes in Compute...

    2022

  16. [16]

    The Satisfiability Modulo Theories Library (SMT-LIB)

    Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016

    2016

  17. [17]

    Barrett, Aaron Stump, and Cesare Tinelli

    Clark W. Barrett, Aaron Stump, and Cesare Tinelli. The smt-lib standard version 2.0. 2010. URL https://api. semanticscholar.org/CorpusID:7943149. Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams 27

    2010

  18. [18]

    Barrett, Roberto Sebastiani, Sanjit A

    Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. InHandbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pages 1267–1329. IOS Press, 2021

    2021

  19. [19]

    Probabilistic relational reasoning for differential privacy

    Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin. Probabilistic relational reasoning for differential privacy. InPOPL, pages 97–110, 2012. doi: 10.1145/2103656.2103670. URL https://dblp.org/rec/conf/popl/ BartheKOB12

    work page doi:10.1145/2103656.2103670 2012

  20. [21]

    Coupling proofs are probabilistic product programs

    Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Coupling proofs are probabilistic product programs. InPOPL, pages 161–174, 2017. doi: 10.1145/3009837.3009896. URL https://dblp.org/rec/conf/popl/ BartheGHS17

    work page doi:10.1145/3009837.3009896 2017

  21. [22]

    A probabilistic separation logic.Proc

    Gilles Barthe, Justin Hsu, and Kevin Liao. A probabilistic separation logic.Proc. ACM Program. Lang., 4(POPL): 55:1–55:30, 2020

    2020

  22. [23]

    Latticed k-induction with an application to probabilistic programs

    Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. Latticed k-induction with an application to probabilistic programs. InCA V (2), volume 12760 ofLecture Notes in Computer Science, pages 524–549. Springer, 2021

    2021

  23. [24]

    Probabilistic program verification via inductive synthesis of inductive invariants

    Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Probabilistic program verification via inductive synthesis of inductive invariants. InTACAS (2), volume 13994 ofLecture Notes in Computer Science, pages 410–429. Springer, 2023

    2023

  24. [25]

    A calculus for amortized expected runtimes.Proc

    Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht. A calculus for amortized expected runtimes.Proc. ACM Program. Lang., 7(POPL):1957–1986, 2023

    1957

  25. [26]

    Foundations for deductive verification of continuous probabilistic programs: From lebesgue to riemann and back.Proc

    Kevin Batz, Joost-Pieter Katoen, Francesca Randone, and Tobias Winkler. Foundations for deductive verification of continuous probabilistic programs: From lebesgue to riemann and back.Proc. ACM Program. Lang., 9(OOPSLA1): 421–448, 2025

    2025

  26. [27]

    Boosting k-induction with continuously-refined invariants

    Dirk Beyer, Matthias Dangl, and Philipp Wendler. Boosting k-induction with continuously-refined invariants. In CA V (1), volume 9206 ofLecture Notes in Computer Science, pages 622–640. Springer, 2015

    2015

  27. [28]

    Randal E. Bryant. Graph-based algorithms for boolean function manipulation.IEEE Trans. Computers, 35(8):677–691, 1986

    1986

  28. [29]

    Burch, Edmund M

    Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 10ˆ20 states and beyond.Inf. Comput., 98(2):142–170, 1992

    1992

  29. [30]

    Termination analysis of probabilistic programs through positivstellensatz’s

    Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. Termination analysis of probabilistic programs through positivstellensatz’s. InCA V (1), pages 3–22, 2016. doi: 10.1007/978-3-319-41528-4\_1. URL https://dblp.org/ rec/conf/cav/ChatterjeeFG16

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

  30. [31]

    Sound and complete certificates for quantitative termination analysis of probabilistic programs

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. Sound and complete certificates for quantitative termination analysis of probabilistic programs. InCA V (1), volume 13371 ofLecture Notes in Computer Science, pages 55–78. Springer, 2022

    2022

  31. [32]

    Quantitative bounds on resource usage of probabilistic programs.Proc

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. Quantitative bounds on resource usage of probabilistic programs.Proc. ACM Program. Lang., 8(OOPSLA1):362–391, 2024. doi: 10.1145/3649824. URL https://dblp.org/rec/journals/pacmpl/ChatterjeeGMZ24

    work page doi:10.1145/3649824 2024

  32. [33]

    Proving almost-sure termination by omega-regular decomposition

    Jianhui Chen and Fei He. Proving almost-sure termination by omega-regular decomposition. InPLDI, pages 869–882,

  33. [34]

    Reactive Probabilistic Programming , booktitle =

    doi: 10.1145/3385412.3386002. URL https://dblp.org/rec/conf/pldi/ChenH20

    work page doi:10.1145/3385412.3386002

  34. [35]

    Counterexample-guided polynomial loop invariant generation by lagrange interpolation

    Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, and Lijun Zhang. Counterexample-guided polynomial loop invariant generation by lagrange interpolation. InCA V (1), volume 9206 ofLecture Notes in Computer Science, pages 658–674. Springer, 2015

    2015

  35. [36]

    Bloem, B

    Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. Approximate counting in smt and value estimation for probabilistic programs. InTACAS, pages 320–334, 2015. doi: 10.1007/978-3-662-46681-0\_26. URL https: //dblp.org/rec/conf/tacas/ChistikovDM15

    work page doi:10.1007/978-3-662-46681-0 2015

  36. [37]

    Approximate counting in smt and value estimation for probabilistic programs.Acta Informatica, 54(8):729–764, 2017

    Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. Approximate counting in smt and value estimation for probabilistic programs.Acta Informatica, 54(8):729–764, 2017. doi: 10.1007/s00236-017-0297-2. URL https: //dblp.org/rec/journals/acta/ChistikovDM17

    work page doi:10.1007/s00236-017-0297-2 2017

  37. [38]

    D’Argenio, Bertrand Jeannet, Henrik Ejersbo Jensen, and Kim Guldstrand Larsen

    Pedro R. D’Argenio, Bertrand Jeannet, Henrik Ejersbo Jensen, and Kim Guldstrand Larsen. Reachability analysis of probabilistic systems by successive refinements. InPAPM-PROBMIV, volume 2165 ofLecture Notes in Computer Science, pages 39–56. Springer, 2001

    2001

  38. [39]

    Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. InTACAS, volume 4963 ofLecture Notes in Computer Science, pages 337–340. Springer, 2008

    2008

  39. [40]

    Dijkstra.A Discipline of Programming

    Edsger W. Dijkstra.A Discipline of Programming. Prentice-Hall, 1976. 28 Daniel Basgöze, Kevin Batz, Sebastian Junges, and Joost-Pieter Katoen

    1976

  40. [41]

    Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümmer

    Alastair F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümmer. Software verification using k-induction. InSAS, volume 6887 ofLecture Notes in Computer Science, pages 351–368. Springer, 2011

    2011

  41. [42]

    Constantin Enea, Rupak Majumdar, Harshit Jitendra Motwani, and V. R. Sathiyanarayana. Verifying almost-sure termination for randomized distributed algorithms.Proc. ACM Program. Lang., 10(POPL):1412–1441, 2026. doi: 10.1145/3776691. URL https://dblp.org/rec/journals/pacmpl/EneaMMS26

    work page doi:10.1145/3776691 2026

  42. [43]

    Probabilistic netkat

    Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic netkat. In Peter Thiemann, editor,Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2...

    work page doi:10.1007/978-3-662-49498-1 2016

  43. [44]

    Gallier.Logic for Computer Science: Foundations of Automatic Theorem Proving

    Jean H. Gallier.Logic for Computer Science: Foundations of Automatic Theorem Proving. Wiley, 1987

    1987

  44. [45]

    Timon Gehr, Sasa Misailovic, and Martin T. Vechev. PSI: exact symbolic inference for probabilistic programs. InCA V (1), volume 9779 ofLecture Notes in Computer Science, pages 62–83. Springer, 2016

    2016

  45. [46]

    Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin T. Vechev. Bayonet: probabilistic inference for networks. InPLDI, pages 586–602. ACM, 2018

    2018

  46. [47]

    Probnv: probabilistic verification of network control planes

    Nick Giannarakis, Alexandra Silva, and David Walker. Probnv: probabilistic verification of network control planes. Proc. ACM Program. Lang., 5(ICFP):1–30, 2021. doi: 10.1145/3473595. URL https://doi.org/10.1145/3473595

    work page doi:10.1145/3473595 2021

  47. [48]

    Gordon, Thomas A

    Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. Probabilistic programming. In FOSE, pages 167–181. ACM, 2014

    2014

  48. [49]

    Haselwarter, Joseph Tassarotti, and Lars Birkedal

    Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. Almost- sure termination by guarded refinement.Proc. ACM Program. Lang., 8(ICFP):203–233, 2024. doi: 10.1145/3674632. URL https://doi.org/10.1145/3674632

    work page doi:10.1145/3674632 2024

  49. [50]

    Haselwarter, Joseph Tassarotti, and Lars Birkedal

    Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. Asynchronous probabilistic couplings in higher-order separation logic.Proc. ACM Program. Lang., 8(POPL):753–784, 2024

    2024

  50. [51]

    Prinsys - on a quest for probabilistic loop invariants

    Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. Prinsys - on a quest for probabilistic loop invariants. In Kaustubh R. Joshi, Markus Siegle, Mariëlle Stoelinga, and Pedro R. D’Argenio, editors,Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, Lecture Notes i...

    work page doi:10.1007/978-3-642-40196-1 2013

  51. [52]

    Jan Friso Groote and Erik P. de Vink. Problem solving using process algebra considered insightful. In Joost-Pieter Katoen, Rom Langerak, and Arend Rensink, editors,ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, volume 10500 ofLecture Notes in Computer Science, pages 48–63. Springer, 2017. doi: 10.1007/978-...

    work page doi:10.1007/978-3-319-68270-9 2017

  52. [53]

    Binary decision diagrams for first-order predicate logic.J

    Jan Friso Groote and Olga Tveretina. Binary decision diagrams for first-order predicate logic.J. Log. Algebraic Methods Program., 57(1-2):1–22, 2003

    2003

  53. [54]

    K-induction without unrolling

    Arie Gurfinkel and Alexander Ivrii. K-induction without unrolling. InFMCAD, pages 148–155. IEEE, 2017

    2017

  54. [55]

    Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal

    Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal. Tachis: Higher-order separation logic with credits for expected costs.Proc. ACM Program. Lang., 8(OOPSLA2):1189–1218, 2024. doi: 10.1145/3689753. URL https://doi.org/10.1145/3689753

    work page doi:10.1145/3689753 2024

  55. [56]

    Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal

    Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal. Approximate relational reasoning for higher-order probabilistic programs.Proc. ACM Program. Lang., 9 (POPL):1196–1226, 2025. doi: 10.1145/3704877. URL https://doi.org/10.1145/3704877

    work page doi:10.1145/3704877 2025

  56. [57]

    Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)

    Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, and Lars Birkedal. Modular verification of differential privacy in probabilistic higher-order separation logic (extended version). CoRR, abs/2604.12713, 2026. doi: 10.48550/ARXIV.2604.12713. URL https://doi.org/10.48550/arXiv.2604.12713

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2604.12713 2026

  57. [58]

    The probabilistic model checker storm.Int

    Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. The probabilistic model checker storm.Int. J. Softw. Tools Technol. Transf., 24(4):589–610, 2022

    2022

  58. [59]

    Bayesian separation logic: A logical foundation and axiomatic semantics for probabilistic programming.Proc

    Shing Hin Ho, Nicolas Wu, and Azalea Raad. Bayesian separation logic: A logical foundation and axiomatic semantics for probabilistic programming.Proc. ACM Program. Lang., 10(POPL):1557–1585, 2026. doi: 10.1145/3776696. URL https://dblp.org/rec/journals/pacmpl/HoWR26

    work page doi:10.1145/3776696 2026

  59. [60]

    Millstein

    Steven Holtzen, Guy Van den Broeck, and Todd D. Millstein. Scaling exact inference for discrete probabilistic programs.Proc. ACM Program. Lang., 4(OOPSLA):140:1–140:31, 2020

    2020

  60. [61]

    Modular verification for almost-sure termination of probabilistic programs.Proc

    Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. Modular verification for almost-sure termination of probabilistic programs.Proc. ACM Program. Lang., 3(OOPSLA):129:1–129:29, 2019. doi: 10.1145/3360555. URL https://dblp.org/rec/journals/pacmpl/Huang0CG19

    work page doi:10.1145/3360555 2019

  61. [62]

    Property-directed k-induction

    Dejan Jovanovic and Bruno Dutertre. Property-directed k-induction. InFMCAD, pages 85–92. IEEE, 2016. Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams 29

    2016

  62. [63]

    PhD thesis, RWTH Aachen University, Germany, 2019

    Benjamin Lucien Kaminski.Advanced Weakest Precondition Calculi for Probabilistic Programs. PhD thesis, RWTH Aachen University, Germany, 2019

    2019

  63. [64]

    Weakest precondition reasoning for expected runtimes of randomized algorithms.J

    Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest precondition reasoning for expected runtimes of randomized algorithms.J. ACM, 65(5):30:1–30:68, 2018

    2018

  64. [65]

    On the hardness of analyzing probabilistic programs.Acta Informatica, 56(3):255–285, 2019

    Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. On the hardness of analyzing probabilistic programs.Acta Informatica, 56(3):255–285, 2019

    2019

  65. [66]

    Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll C. Morgan. Linear-invariant generation for probabilistic programs: - automated support for proof-based methods. In Radhia Cousot and Matthieu Martel, editors,Static Analysis - 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010. Proceedings, Lecture Notes in ...

    work page doi:10.1007/978-3-642-15769-1 2010

  66. [67]

    Barrett, and Cesare Tinelli

    Tim King, Clark W. Barrett, and Cesare Tinelli. Leveraging linear and mixed integer programming for SMT. In FMCAD, pages 139–146. IEEE, 2014

    2014

  67. [68]

    Automated verification of higher-order probabilistic programs via a dependent refinement type system.Proc

    Satoshi Kura and Hiroshi Unno. Automated verification of higher-order probabilistic programs via a dependent refinement type system.Proc. ACM Program. Lang., 8(ICFP):973–1002, 2024. doi: 10.1145/3674662. URL https: //dblp.org/rec/journals/pacmpl/0001024

    work page doi:10.1145/3674662 2024

  68. [69]

    A hierarchy of supermartingales for 𝜔-regular verification

    Satoshi Kura and Hiroshi Unno. A hierarchy of supermartingales for 𝜔-regular verification. 10(PLDI), June 2026. doi: 10.1145/3808257

    work page doi:10.1145/3808257 2026

  69. [70]

    Ranking and invariants for lower-bound inference in quantitative verification of probabilistic programs.CoRR, abs/2504.04132, 2025

    Satoshi Kura, Hiroshi Unno, and Takeshi Tsukada. Ranking and invariants for lower-bound inference in quantitative verification of probabilistic programs.CoRR, abs/2504.04132, 2025

    Pith/arXiv arXiv 2025

  70. [71]

    Supermartingales for unique fixed points: A unified approach to lower bound verification.Proc

    Satoshi Kura, Hiroshi Unno, and Takeshi Tsukada. Supermartingales for unique fixed points: A unified approach to lower bound verification.Proc. ACM Program. Lang., 10(PLDI), June 2026. doi: 10.1145/3808348

    work page doi:10.1145/3808348 2026

  71. [72]

    Eyal Kushilevitz and Michael O. Rabin. Randomized mutual exclusion algorithms revisited. InPODC, pages 275–283. ACM, 1992

    1992

  72. [73]

    Probta: A sound and complete proof rule for probabilistic verification.CoRR, abs/2203.04422, 2022

    Guanyan Li, Zhilei Han, and Fei He. Probta: A sound and complete proof rule for probabilistic verification.CoRR, abs/2203.04422, 2022. doi: 10.48550/arXiv.2203.04422. URL https://dblp.org/rec/journals/corr/abs-2203-04422

    work page doi:10.48550/arxiv.2203.04422 2022

  73. [74]

    Structural abstraction and refinement for probabilistic programs.CoRR, abs/2508.12344, 2025

    Guanyan Li, Juanen Li, Zhilei Han, Peixin Wang, Hongfei Fu, and Fei He. Structural abstraction and refinement for probabilistic programs.CoRR, abs/2508.12344, 2025

    arXiv 2025

  74. [75]

    Structural abstraction and refinement for probabilistic programs.Proc

    Guanyan Li, Juanen Li, Zhilei Han, Peixin Wang, Hongfei Fu, and Fei He. Structural abstraction and refinement for probabilistic programs.Proc. ACM Program. Lang., 9(OOPSLA2):1809–1836, 2025. doi: 10.1145/3763115. URL https://dblp.org/rec/journals/pacmpl/LiLHW0025

    work page doi:10.1145/3763115 2025

  75. [76]

    Haselwarter, Joseph Tassarotti, and Lars Birkedal

    Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. Modular reasoning about error bounds for concurrent probabilistic programs.Proc. ACM Program. Lang., 9 (ICFP):276–305, 2025. doi: 10.1145/3747514. URL https://doi.org/10.1145/3747514

    work page doi:10.1145/3747514 2025

  76. [77]

    Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)

    Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal. Contextual refinement of higher-order concurrent probabilistic programs.CoRR, abs/2511.10135, 2025. doi: 10.48550/ARXIV.2511.10135. URL https: //doi.org/10.48550/arXiv.2511.10135

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2511.10135 2025

  77. [78]

    Rupak Majumdar and V. R. Sathiyanarayana. Positive almost-sure termination: Complexity and proof rules.Proc. ACM Program. Lang., 8(POPL):1089–1117, 2024. doi: 10.1145/3632879. URL https://dblp.org/rec/journals/pacmpl/ MajumdarS24

    work page doi:10.1145/3632879 2024

  78. [79]

    Rupak Majumdar and V. R. Sathiyanarayana. Sound and complete proof rules for probabilistic termination.Proc. ACM Program. Lang., 9(POPL):1871–1902, 2025. doi: 10.1145/3704899. URL https://dblp.org/rec/journals/pacmpl/ MajumdarS25

    work page doi:10.1145/3704899 1902

  79. [80]

    Modular specifications and implemen- tations of random samplers in higher-order separation logic

    Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, and Lars Birkedal. Modular specifications and implemen- tations of random samplers in higher-order separation logic. In Kathrin Stark, Yannick Zakowski, Nikhil Swamy, and Nicolas Tabareau, editors,Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 20...

    work page doi:10.1145/3779031.3779109 2026

  80. [81]

    Monographs in Computer Science

    Annabelle McIver and Carroll Morgan.Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005

    2005

Showing first 80 references.