Pith. sign in

REVIEW 2 major objections 6 minor 29 references

Towards a Proof System for Probabilistic Dynamic Logic

T0 review · 2 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper establishes a sound forward symbolic-execution proof system for probabilistic dynamic logic.

desk verdict A soundness proof for a forward symbolic-execution calculus for pDL, credible but with a domain gap around almost-sure termination and loop rules still sketched. read the letter →

arxiv 2412.00906 v1 pith:YHJVQRXZ submitted 2024-12-01 cs.LO

Einar Broch Johnsen , Eduard Kamburjan , Raúl Pardo , Erik Voogd , Andrzej Wąsowski This is my paper · ORCID
classification cs.LO MSC 03B7068Q60
keywords probabilisticdynamiclogicpGCLsymbolicexecutiondeductiveverificationprogramsMarkovdecisionprocessessoundnessconstraints
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper reports work in progress on a deductive proof system for probabilistic dynamic logic (pDL), a specification logic for programs in the probabilistic guarded command language pGCL. The paper's central claim is that the proposed proof system is sound: every judgment derivable by its symbolic-execution rules is valid in the pDL semantics, so the rules produce only correct probabilistic specifications. The proof system works forward, symbolically executing the program and collecting constraints on probability lower bounds as side conditions; closing a proof then reduces to checking those constraints. A prototype built on an existing symbolic execution engine and an SMT solver is used to verify a pDL specification of the Monty Hall game, showing the approach in action.

What carries the argument

The central object is the symbolic-execution judgment $\Gamma \vdash U\,[s]_p\,\varphi$ together with the pDL-constraints attached to the branching rules. Symbolic updates $U$ are syntactic substitutions that record state changes without evaluating them, a technique taken from dynamic-logic verification; pDL-constraints are inequalities over probability variables that must hold under the current update and assumptions. The rules for demonic and probabilistic choice generate the constraints $p \leq \min(p_1,p_2)$ and $p \leq e\cdot p_1 + (1-e)\cdot p_2$, respectively, and these constraints are what carry the probabilistic content of the proof. The soundness argument connects each rule to the corresponding MDP semantics of pGCL through the properties of pDL listed in Proposition 1.

What would settle it

Exhibit one pGCL program that is almost surely terminating and one closed proof tree in the calculus whose root judgment $\Gamma \vdash \varphi$ is false in the pDL semantics for some valuation satisfying $\Gamma$; Theorem 1 would then be false. Concretely, one could instrument the prototype to output every closed proof and independently compute the minimal reachability probability of the program by MDP model checking, looking for a mismatch.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that forward symbolic execution can be organized into a sound deductive calculus for pDL. The calculus operates on judgments $\Gamma \vdash U\,[s]_p\,\varphi$, where $U$ is a symbolic update describing the current abstract state, $s$ is the remaining program, and $p$ is a lower bound on the probability that $\varphi$ holds after $s$. Each rule in the rule set corresponds to one pGCL construct: assignment is turned into an update, demonic choice takes the minimum of branch probabilities, probabilistic choice takes the probability-weighted sum, and while loops are unfolded once. The side conditions are pDL-constraints on the probability variables, and a proof closes when the accumulated constraints are satisfiable. Theorem 1 states that any closed proof tree yields a valid pDL formula; the proof goes by induction on proof-tree height using the pDL properties collected in the paper's Proposition 1.

Load-bearing premise

The semantics and the proof system apply only to programs that terminate with probability 1 under every policy; if a program can loop forever with nonzero probability, the expected rewards in the pDL semantics are undefined and soundness no longer applies.

Editorial extensions

If this is right

  • Any specification proved with the calculus is guaranteed to be a valid pDL formula, so verified lower bounds on reachability probabilities are trustworthy.
  • The calculus supports forward reasoning, meaning proofs can be automated by symbolic execution and the remaining arithmetic sent to an SMT solver.
  • Because pDL is closed under logical operators, the proof system can express properties beyond Hoare logic, such as program equivalence relative to state formulae.
  • The current loop handling is a single unrolling rule, so general reasoning about probabilistic loops remains an explicitly open problem for this forward framework.
  • The Monty Hall example demonstrates that the method can handle nested nondeterministic and probabilistic choices and produce a closed proof with satisfiable probability constraints.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If soundness extends to richer loop rules, the same constraint-accumulation scheme could provide a forward counterpart to weakest-precondition calculi for expected values and expected runtimes.
  • Because the semantics assumes almost-sure termination, the proof system cannot by itself establish termination; a termination certificate would need to be supplied separately.
  • The approach could be compared against weakest-precondition engines on a benchmark of pGCL programs to measure proof size and automation, though the paper does not report such a comparison.
  • Adding observe-statements to pGCL and encoding conditioning as probabilistic constraints could connect this deductive style to verification of Bayesian inference programs.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The paper introduces a deductive proof system for Pardo et al.'s probabilistic dynamic logic (pDL) over the probabilistic guarded command language pGCL. The proof system follows KeY-style forward symbolic execution: judgments of the form Γ ⊢ U[s]_p φ are proved by syntax-driven rules (Figure 3) that accumulate side constraints on probability variables, and a proof tree is closed when the resulting constraint set is satisfiable. The main formal result is Theorem 1, which claims soundness of the Figure 3 calculus: every derivable judgment is valid in the pDL semantics. The paper illustrates the approach on the Monty Hall program and reports on a prototype implementation built on Crowbar and Z3.

Significance. If the formal gaps are repaired, the paper would provide a forward-reasoning proof system for pDL, complementing the backward weakest-precondition style of Katoen and collaborators and exploiting the expressive strength of dynamic logic. The manuscript's strengths include an explicit soundness proof organized rule-by-rule, a nontrivial worked example, and a publicly available prototype implementation. The paper is honest in labeling itself work in progress, and the authors clearly identify the loop-handling problem as an open issue. However, the soundness theorem is not yet stated at the required level of rigor: the almost-sure termination assumption is not integrated into the theorem, and the probability-variable machinery used by the rules is not formally part of the pDL syntax. These issues are local and fixable, but they currently undermine the central claim.

major comments (2)
  1. [§3.1, Theorem 1, Eq. (3), Figure 3] Theorem 1 states that for all Γ and φ, if Γ ⊢ φ then |= (∧Γ) → φ, with no side condition restricting φ to programs that satisfy the almost-sure termination assumption introduced in Section 3.1. The expectation in Eq. (3) is only defined when every policy reaches a final state with probability 1, and the text explicitly says that pDL 'can only talk about properties of almost surely terminating programs.' The calculus in Figure 3 contains no rule or side condition that checks almost-sure termination; loopUnroll merely unfolds a while-loop into a conditional. Consequently, the validity relation in the theorem's conclusion is undefined for any derivable judgment whose program violates the assumption, and the theorem is formally ill-posed as written. The theorem should be restated with an explicit hypothesis that all programs occurring in φ are almost surely terminating under all policies, or the calculus should be restricted to such programs.
  2. [§4.1, §5 (Judgments), Figure 3] The proof rules in Figure 3 use p, p1, and p2 as syntactic probability variables in constraints such as ⟨p ≤ min(p1, p2)⟩, and the surrounding text speaks of solving these constraints. However, the pDL syntax in Section 4.1 has no category for probability terms or probability variables: p is introduced as a semantic object p : State → [0,1]. The paper never defines the syntax of judgments with free probability variables, nor the satisfaction of a formula [s]_p φ when p is a variable rather than an expectation function. This makes both the constraint-satisfiability condition and the quantification 'for all Γ and φ' in Theorem 1 undefined. The authors should add a formal language of probability parameters/terms, their interpretation, and the semantics of judgments relative to assignments of those parameters.
minor comments (6)
  1. [§2] The sentence 'for x, y ∈ {0, 1, 2}, the expression z = (2x − y) mod 3 simply returns z ∈ {0, 1, 2} such that z ≠ x and z ≠ y' is false when x = y; it should be stated with the side condition x ≠ y, which is the case in the else-branch where the expression is used.
  2. [§4.2] The text 'We use |= [s]_p φ to denote that a formula is valid' conflates the satisfaction relation with the validity relation; a metalinguistic symbol such as ⊨ should be used for validity.
  3. [Figure 3] In the loopUnroll rule, the premise contains an unbalanced closing bracket: 'U[if (e) {sb; while (e) {sb}; s} else s}]p φ' should read 'U[if (e) {sb; while (e) {sb}; s} else s]_p φ'.
  4. [§5] The sentence defining judgments uses 'V Γ' where the conjunction symbol is intended, and the 'Probabilistic constraints' paragraph contains a doubled 'that that'; both need correction.
  5. [§5] The assertion 'Γ ⊢ φ expresses existence of a proof tree' should specify that proof trees are finite and define the height used in the induction for Theorem 1; otherwise the induction over proof-tree height is not formally grounded.
  6. [§6] The paper should state explicitly which rules of Figure 3 are supported by the Crowbar prototype; the reported example is loop-free, and it is unclear whether the loopUnroll rule has been implemented or tested.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the soundness proof verifies each rule directly against the pDL semantics; the prior-work Proposition 1 is independent support, and the almost-sure-termination restriction is a scope caveat, not a circular step.

full rationale

The derivation chain is not circular. The paper defines pDL semantics in Definition 2 (Section 4.2) and then states Proposition 1 (Properties of pDL [25]) as semantic facts about that semantics. The proof system's rules in Figure 3 are justified in Theorem 1 by induction over proof trees, checking each rule against Definition 2 and Proposition 1. None of the rules is assumed as an axiom inside the semantics, and the soundness proof does not invoke Theorem 1 or the proof system's derivability as a hypothesis. For example, the loopUnroll rule is proven directly from the operational MDP rules (While1/While2, If1/If2, Composition) and the definition of expectation, rather than by quoting Proposition 1(x). The only self-citation is Proposition 1 from [25] by overlapping authors; it is used in the soundness proof, but it is a parameter-free published theorem about the semantics whose stated assumptions (almost-sure termination) do not include the target soundness claim, so it counts as independent support under the review rules and does not raise the circularity score. The paper explicitly restricts the logic to almost surely terminating programs (Section 3.1: 'we assume that MDPs (and the programs we derive them from) arrive at final states with probability 1 under all policies'), and the loopUnroll rule does not itself check this restriction; a finite proof tree would appear to require finite unrolling, but the paper does not prove that derivability implies membership in the semantic domain. This is a scope/correctness gap, not a circularity. The Monty Hall example is not a fitted prediction: the probabilistic constraints are generated by symbolic execution and discharged by Z3, with the 2/3 result arising from the constraints rather than being presupposed. Overall, no step in the claimed derivation reduces by construction to its own input.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The calculus adds no free parameters: probability variables are logical variables instantiated by the SMT solver. The central claim rests on the almost-sure termination assumption and on the state-independence of probabilistic choice probabilities, both stated in the paper. The soundness proof leans on Proposition 1 from the authors' earlier paper [25], which is a legitimate external result but should be checked for consistency with the semantics defined here.

assumptions (4)
  • domain assumption Programs are almost surely terminating under all policies.
    Stated in Section 3.1: 'we assume that MDPs (and the programs we derive them from) arrive at final states with probability 1 under all policies.' The pDL semantics and the soundness proof rely on this to define expectations over finite paths.
  • domain assumption Probabilistic expressions in pDL specifications do not depend on state variables.
    Stated in Section 5 (Probabilistic constraints): 'we introduce the simplifying assumption that probabilistic expressions in pDL do not depend on state variables, in which case we can simplify constraints to simple (in)equalities.' This is used in the constraint generation and discharge.
  • standard math The MDP semantics for pGCL (Figure 2) correctly captures the operational behavior.
    The proof system's rules are proven sound relative to this semantics; it is a standard encoding of pGCL.
  • domain assumption Proposition 1 (Properties of pDL) holds.
    The soundness proof repeatedly invokes Proposition 1, which is stated as from [25]. If this proposition were false, the proof system's rules would be unsound.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards a Proof System for Probabilistic Dynamic Logic." pith.science (2026). https://pith.science/paper/YHJVQRXZ

@misc{pith2026241200906,
  author       = {Pith},
  title        = {Pith review of: Towards a Proof System for Probabilistic Dynamic Logic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YHJVQRXZ}},
  note         = {Machine review of arXiv:2412.00906}
}
read the original abstract

Whereas the semantics of probabilistic languages has been extensively studied, specification languages for their properties have received less attention -- with the notable exception of recent and on-going efforts by Joost-Pieter Katoen and collaborators. In this paper, we revisit probabilistic dynamic logic (pDL), a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. Building on dynamic logic, pDL can express both first-order state properties and probabilistic reachability properties. In this paper, we report on work in progress towards a deductive proof system for pDL. This proof system, in line with verification systems for dynamic logic such as KeY, is based on forward reasoning by means of symbolic execution.

Figures

Figures reproduced from arXiv: 2412.00906 by the authors.

Figure 1
Figure 1. The Monty Hall Program in pGCL (Monty_Hall). This paper revisits pDL and its model-theoretic semantics, and its main con￾tribution is a deductive verification system for pDL based on forward reasoning about pDL judgments, in contrast to the backwards reasoning used in weakest￾precondition-based approaches. To this aim, we sketch a proof system for pDL based on symbolic execution rules that collect constraints about … view at source ↗
Figure 2
Figure 2. An MDP-semantics for pGCL. some initial valuation ε and the state ⟨ε, skip⟩ represents a final state in which the program has terminated with the valuation ε. For a concrete program, the policy π is a function that determines how non-deterministic choice is resolved for a given valuation of the program variables; i.e., π⟨ε, s1 ⊓ s2⟩ = si for either i = 1 or i = 2. The rules defining the partial transition probabilit… view at source ↗
Figure 3
Figure 3. Symbolic execution rules. and Composition2 and the fact that ε |= e, also p ≤ Eε[[φ]] for s1; s. Then, using Rule If1 and ε |= e again, p ≤ Eε[[φ]] in (if (e){s1} else {s2}); s, so that ε |= [(if (e){s1} else {s2}); s]pφ, and so ε ′ |= U[(if (e){s1} else {s2}); s]pφ. – Finally, for rule loopUnroll, let ε ′ be arbitrary and let ε = ρU (ε ′ ). There are two cases to consider: • If ε |= e (meaning ε(e) = true) then: ε … view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: The Monty Hall game in the ABS encoding for Crowbar. solve arithmetic constraints: Crowbar performs the symbolic execution and uses Z3 to discharge formulas without modalities. Crowbar was originally developed to experiment with deductive proof systems for the active o…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 14 canonical work pages

  1. [25]

    In: Proc

    Pardo, R., Johnsen, E.B., Schaefer, I., Wąsowski, A.: A specification logic for programs in the probabilistic guarded command language. In: Proc. 19th In- ternational Colloquium on Theoretical Aspects of Computing (ICTAC’22). Lec- ture Notes in Computer Science, vol. 13572, pp. 369–387. Springer (2022), https://doi.org/10.1007/978-3-031-17715-6_24

    work page doi:10.1007/978-3-031-17715-6_24 2022

  2. [1]

    (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol

    Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol. 10001. Springer (2016),https://doi.org/10.1007/ 978-3-319-49812-6

    work page 2016

  3. [2]

    IEEE Trans

    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng.29(6), 524–541 (2003), https://doi.org/10.1109/TSE.2003.1205180

    arXiv 2003

  4. [3]

    MIT Press (2008)

    Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)

    work page 2008

  5. [4]

    In: Baeten, J.C.M., Mauw, S

    Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) Proc. 10th International Conference on Concurrency Theory (CONCUR’99). Lecture Notes in Computer Science, vol. 1664, pp. 146–161. Springer (1999),https://doi.org/10.1007/ 3-540-48320-9_12

    work page 1999

  6. [5]

    Batz, K., Biskup, T.J., Katoen, J.-P., Winkler, T.: Programmatic strategy synthesis: Resolving nondeterminism in probabilistic programs. Proc. ACM Program. Lang. 8(POPL), 2792–2820 (2024),https://doi.org/10.1145/3632935

    doi:10.1145/3632935 2024

  7. [6]

    In: Sankaranarayanan, S., Sharygina, N

    Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J.-P., Matheja, C.: Prob- abilistic program verification via inductive synthesis of inductive invariants. In: Sankaranarayanan, S., Sharygina, N. (eds.) Proc. 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023). Lecture Notes in Computer Sci...

    doi:10.1007/978-3-031-30820-8_25 2023

  8. [7]

    Batz, K., Kaminski, B.L., Katoen, J.-P., Matheja, C.: Relatively complete verifica- tion of probabilistic programs: an expressive language for expectation-based reason- ing. Proc. ACM Program. Lang.5(POPL), 1–30 (2021),https://doi.org/10.1145/3434320

    work page doi:10.1145/3434320 2021

Show all 29 references
  1. [8]

    In: Ahrendt et al

    Beckert, B., Klebanov, V., Weiß, B.: Dynamic logic for Java. In: Ahrendt et al. [1], pp. 49–106, https://doi.org/10.1007/978-3-319-49812-6_3

    doi

  2. [9]

    Formal Aspects of Computing33(4), 617–636 (2021),https://doi.org/10.1007/s00165-020-00527-y 16 E.B

    de Boer, F.S., Bonsangue, M.: Symbolic execution formally explained. Formal Aspects of Computing33(4), 617–636 (2021),https://doi.org/10.1007/s00165-020-00527-y 16 E.B. Johnsen et al

    2021 doi

  3. [10]

    In: Majumdar, R., Kuncak, V

    Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: A modern probabilistic model checker. In: Majumdar, R., Kuncak, V. (eds.) Proc. 29th International Conference on Computer Aided Verification (CAV 2017). Lecture Notes in Computer Science, vol. 10427, pp. 592–...

    2017

  4. [11]

    Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J.-P., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA1), 696–726 (2023),https://doi.org/10.1145/3586051

    2023 doi

  5. [12]

    In: Apt, K.R., Hoare, T

    Hähnle, R.: Dijkstra’s legacy on program verification. In: Apt, K.R., Hoare, T. (eds.) Edsger Wybe Dijkstra: His Life, Work, and Legacy, pp. 105–140. ACM / Morgan & Claypool (2022),https://doi.org/10.1145/3544585.3544593

    2022

  6. [13]

    Foundations of Computing, MIT Press (Oct 2000)

    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Foundations of Computing, MIT Press (Oct 2000)

    2000

  7. [14]

    Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf.24(4), 589–610 (2022), https://doi.org/10.1007/s10009-021-00633-z

    2022 doi

  8. [15]

    In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M

    Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Proc. 9th International Symposium on Formal Methods for Components and Objects (FMCO 2010)....

    2010 doi

  9. [16]

    Formal Methods Syst

    Junges, S., Ábrahám, E., Hensel, C., Jansen, N., Katoen, J.-P., Quatmann, T., Volk, M.: Parameter synthesis for Markov models: covering the parameter space. Formal Methods Syst. Des.62(1), 181–259 (2024),https://doi.org/10.1007/s10703-023-00442-x

    2024 doi

  10. [17]

    Kamburjan, E., Scaletta, M., Rollshausen, N.: Deductive verification of active objects with Crowbar. Sci. Comput. Program.226, 102928 (2023),https://doi.org/10. 1016/j.scico.2023.102928

    2023

  11. [18]

    Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. Ph.D. thesis, RWTH Aachen University, Germany (2019),http://publications.rwth-aachen. de/record/755408

    2019

  12. [19]

    Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM65(5), 30:1– 30:68 (2018), https://doi.org/10.1145/3208102

    2018 doi

  13. [20]

    In: Proc

    Kozen, D.: Semantics of probabilistic programs. In: Proc. 20th Annual Symposium on Foundations of Computer Science. pp. 101–114. IEEE Computer Society (1979), https://doi.org/10.1109/SFCS.1979.38

    1979 doi

  14. [21]

    Monographs in Computer Science, Springer (2005),https://doi.org/10.1007/ b138392

    McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer (2005),https://doi.org/10.1007/ b138392

    2005

  15. [22]

    McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.-P.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang.2(POPL), 33:1–33:28 (2018), https://doi.org/10.1145/3158121

    2018 doi

  16. [23]

    In: Ramakrishnan, C.R., Rehof, J

    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Sp...

    2008 doi

  17. [24]

    In: Jobstmann, B., Leino, K.R.M

    Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) Proc. 17th International Conference on Verification, Model Checking, and Abstract Towards a Proof System for Probabilistic Dy...

    2016 doi

  18. [26]

    Wiley (2005)

    Puterman, M.L.: Markov Decision Processes. Wiley (2005)

    2005

  19. [27]

    Schlatte, R., Johnsen, E.B., Kamburjan, E., Tapia Tarifa, S.L.: The ABS simulator toolchain. Sci. Comput. Program.223, 102861 (2022),https://doi.org/10.1016/j.scico.2022. 102861

    2022 doi

  20. [28]

    Schröer, P., Batz, K., Kaminski, B.L., Katoen, J.-P., Matheja, C.: A deductive verification infrastructure for probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA2), 2052–2082 (2023),https://doi.org/10.1145/3622870

    2023 doi

  21. [29]

    In: Jansen, N., Tribastone, M

    Voogd, E., Johnsen, E.B., Silva, A., Susag, Z.J., Wąsowski, A.: Symbolic seman- tics for probabilistic programs. In: Jansen, N., Tribastone, M. (eds.) Proc. 20th International Conference on Quantitative Evaluation of Systems (QEST 2023). Lecture Notes in Computer Science, vol....

    2023 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.