Pith. sign in

REVIEW 3 major objections 1 minor 52 references

Quantitative Verification with Neural Networks

T0 review · 3 major / 1 minor · reviewed 2026-05-24 · grok-4.3

Challenge this review Download PDF Read on arXiv ↗

Pith's one-line read Neural networks serve as supermartingale certificates to compute sound probability bounds for stochastic processes via a CEGIS loop with SMT verification.

desk verdict Neural CEGIS for supermartingale certificates works on some hard benchmarks but the loop has no termination guarantee. read the letter →

arxiv 2301.06136 v7 submitted 2023-01-15 cs.LO cs.PLcs.SYeess.SY

Alessandro Abate , Alec Edwards , Mirco Giacobbe , Hashan Punchihewa , Diptarko Roy This is my paper
classification cs.LOcs.PLcs.SYeess.SY
keywords neuralnetworkssupermartingalesquantitativeverificationprobabilisticprogramsstochasticdynamicalmodelsCEGISSMTsolversreachabilityanalysis
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

The paper develops a data-driven method for quantitative verification of probabilistic programs and stochastic dynamical models by computing tight upper bounds on the probability of hitting a target condition in finite time. It trains neural networks to represent supermartingales that certify these bounds, using stochastic optimization on sampled states to tighten the bound while a satisfiability modulo theories solver checks the certificate over the entire state space. Counterexamples from the solver are added to the training set, repeating until the certificate is formally valid. The approach targets problems including reachability and safety analysis as well as assertion violation and termination checking.

What carries the argument

The counterexample-guided inductive synthesis loop that trains neural networks as supermartingales on samples and verifies them with SMT solvers over the full state space.

What would settle it

An instance of a stochastic model with a known true hitting probability where the synthesized neural supermartingale is accepted by the SMT solver yet the reported bound is violated by an actual trajectory, or where the loop fails to terminate on a model with computable bounds.

Watch

Extended reading notes

Core claim

Neural networks can represent supermartingale certificates whose validity yields sound probability bounds; these certificates are synthesized through a counterexample-guided inductive synthesis loop that alternates stochastic optimization to tighten bounds on samples with SMT checks for validity over every state, terminating with a confirmed certificate when no counterexamples remain.

Load-bearing premise

Neural networks can be trained to represent supermartingales that SMT solvers confirm as valid over the entire continuous or discrete state space without the training loop diverging or producing invalid or overly loose bounds.

Editorial extensions

If this is right

  • The method produces smaller or comparable probability bounds than existing symbolic techniques across tested benchmarks.
  • It succeeds on models that lie entirely beyond the reach of symbolic methods.
  • The same framework applies uniformly to reachability and safety of stochastic dynamical models as well as assertion violation and termination of probabilistic programs.

Reading between the lines

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

  • The reliance on neural expressivity suggests the technique could scale to higher-dimensional or hybrid systems where manual symbolic certificate construction becomes intractable.
  • Because the loop separates sampling-based tightening from formal verification, it may be combined with other certificate classes beyond supermartingales for different quantitative properties.
  • Success on previously intractable models indicates that data-driven certificate search can reduce dependence on hand-crafted templates in probabilistic verification workflows.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 1 minor

Summary. The paper presents a data-driven method for quantitative verification of probabilistic programs and stochastic dynamical models. It uses neural networks to represent supermartingale certificates that provide sound upper bounds on the probability of hitting a target condition in finite time. These certificates are synthesized via a counterexample-guided inductive synthesis (CEGIS) loop that alternates stochastic optimization on state-space samples with SMT-based validity checks over the full domain; counterexamples are added until the certificate is confirmed valid. The approach is evaluated on a diverse set of benchmarks, where it produces smaller or comparable bounds to symbolic methods and succeeds on models beyond the reach of those techniques.

Significance. If the empirical results hold under the stated assumptions, the work is significant for extending formal verification to complex probabilistic systems that are intractable for symbolic techniques. The combination of neural expressiveness with SMT-based certification is a notable strength, as is the reproducible evaluation across benchmarks that includes cases unreachable by alternatives. This could influence hybrid ML-formal methods in verification, provided the CEGIS procedure's reliability is better substantiated.

major comments (3)
  1. [Abstract] Abstract and method description: The claim that the produced bounds are sound and that the method succeeds on benchmarks unreachable by symbolic tools provides no derivation details, error-bar analysis, or description of how post-training SMT queries are formulated to verify supermartingale conditions over the entire state space; this is load-bearing for the soundness assertion.
  2. [CEGIS loop description] CEGIS loop section: The procedure is described as repeating 'until validity is confirmed,' but no argument or condition is supplied showing that a neural network in the chosen architecture class exists that satisfies the supermartingale drift and boundary conditions tightly enough for SMT to decide validity without divergence or excessive looseness; termination therefore rests solely on empirical success.
  3. [Experimental evaluation] Experimental evaluation: While the paper reports that the method yields smaller or comparable bounds in all cases, there is no analysis of bound sensitivity to training hyperparameters or multiple independent runs, which is needed to substantiate the cross-benchmark claim that the approach is reliably tighter or more scalable than symbolic alternatives.
minor comments (1)
  1. [Preliminaries] Notation for the supermartingale conditions and probability bound could be clarified with an explicit equation relating the NN output to the hitting probability.

Simulated Author's Rebuttal

3 responses · 1 unresolved

We thank the referee for the detailed and constructive report. We address each major comment below. The manuscript already contains the core technical details on soundness and SMT encoding in Sections 3 and 4, but we agree that additional exposition and experimental analysis would strengthen the presentation.

read point-by-point responses

  1. Referee: [Abstract] Abstract and method description: The claim that the produced bounds are sound and that the method succeeds on benchmarks unreachable by symbolic tools provides no derivation details, error-bar analysis, or description of how post-training SMT queries are formulated to verify supermartingale conditions over the entire state space; this is load-bearing for the soundness assertion.

    Authors: Soundness follows directly from the supermartingale theorem (Theorem 1 in the paper) once the SMT solver confirms that the neural network satisfies the drift and boundary conditions everywhere; the SMT queries encode the network as a piecewise-linear or polynomial function (depending on activation) together with the one-step expectation operator of the stochastic model, which is itself expressible in the theory of real arithmetic. This encoding is described in Section 4.2. Because verification is exhaustive rather than statistical, error bars are not applicable. We will revise the method description to include a short paragraph summarizing the SMT encoding and will add a sentence to the abstract referencing the soundness argument. revision: partial

  2. Referee: [CEGIS loop description] CEGIS loop section: The procedure is described as repeating 'until validity is confirmed,' but no argument or condition is supplied showing that a neural network in the chosen architecture class exists that satisfies the supermartingale drift and boundary conditions tightly enough for SMT to decide validity without divergence or excessive looseness; termination therefore rests solely on empirical success.

    Authors: We do not claim a general existence or termination guarantee for the CEGIS loop; the procedure is a practical synthesis method whose success depends on the expressiveness of the chosen neural architecture and the quality of the counterexample feedback. When the loop terminates with a valid certificate, the resulting bound is sound by construction. We will add an explicit statement in Section 3.3 acknowledging that termination is not theoretically guaranteed and is observed empirically on the evaluated benchmarks. revision: yes

  3. Referee: [Experimental evaluation] Experimental evaluation: While the paper reports that the method yields smaller or comparable bounds in all cases, there is no analysis of bound sensitivity to training hyperparameters or multiple independent runs, which is needed to substantiate the cross-benchmark claim that the approach is reliably tighter or more scalable than symbolic alternatives.

    Authors: The current evaluation reports results from the final verified certificates on each benchmark. To address sensitivity, we will add a new subsection (or appendix) reporting bound variation across a modest grid of learning rates and network widths, together with results from three independent training seeds per benchmark. This will provide quantitative support for the reliability claim. revision: yes

standing simulated objections not resolved
  • No general argument is available showing that a neural network of the chosen architecture class is guaranteed to exist that satisfies the supermartingale conditions with sufficient tightness for the SMT solver to succeed without excessive looseness or non-termination.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; bounds derived from verified supermartingale properties

full rationale

The paper's central derivation uses a CEGIS loop to train a neural network approximating a supermartingale certificate, followed by SMT-based validity check over the full state space. When the SMT check succeeds, the probability bound follows directly from the standard supermartingale theorem (soundness is external to the training). No equation or step equates the output bound to a fitted parameter by construction, nor does any load-bearing premise reduce to a self-citation chain. The method is algorithmic and the claimed soundness is conditional on successful verification rather than on re-deriving the input data.

Assumptions & free parameters 1 free parameters · 2 assumptions · 0 invented entities

The central claim rests on the existence of supermartingales that can be represented by neural networks and verified by SMT; the paper introduces no new physical entities but relies on standard martingale theory and the decidability of the SMT queries used in the loop.

free parameters (1)
  • neural network architecture and training hyperparameters
    Chosen by the authors to represent supermartingales; their specific values are not reported in the abstract.
assumptions (2)
  • domain assumption Supermartingales yield sound upper bounds on finite-time hitting probabilities for stochastic processes
    Invoked when the authors state that neural networks represent supermartingale certificates that yield such probability bounds.
  • domain assumption SMT solvers can decide validity of the neural certificate over the entire state space
    Invoked in the description of the counterexample-guided inductive synthesis loop.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Quantitative Verification with Neural Networks." pith.science (2026). https://pith.science/paper/2301.06136

@misc{pith2026230106136,
  author       = {Pith},
  title        = {Pith review of: Quantitative Verification with Neural Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2301.06136}},
  note         = {Machine review of arXiv:2301.06136}
}
read the original abstract

We present a data-driven approach to the quantitative verification of probabilistic programs and stochastic dynamical models. Our approach leverages neural networks to compute tight and sound bounds for the probability that a stochastic process hits a target condition within finite time. This problem subsumes a variety of quantitative verification questions, from the reachability and safety analysis of discrete-time stochastic dynamical models, to the study of assertion-violation and termination analysis of probabilistic programs. We rely on neural networks to represent supermartingale certificates that yield such probability bounds, which we compute using a counterexample-guided inductive synthesis loop: we train the neural certificate while tightening the probability bound over samples of the state space using stochastic optimisation, and then we formally check the certificate's validity over every possible state using satisfiability modulo theories; if we receive a counterexample, we add it to our set of samples and repeat the loop until validity is confirmed. We demonstrate on a diverse set of benchmarks that, thanks to the expressive power of neural networks, our method yields smaller or comparable probability bounds than existing symbolic methods in all cases, and that our approach succeeds on models that are entirely beyond the reach of such alternative techniques.

Discussion (0). Sign in to comment.

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

52 extracted references · 52 canonical work pages

  1. [1]

    Formal synthesis of Lyapunov neural networks

    Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. Formal synthesis of Lyapunov neural networks. IEEE Control. Syst. Lett. , 5(3):773--778, 2021

    work page 2021

  2. [2]

    Quantitative verification with neural networks

    Alessandro Abate, Alec Edwards, Mirco Giacobbe, Hashan Punchihewa, and Diptarko Roy. Quantitative verification with neural networks. In CONCUR , volume 279 of LIPIcs , pages 22:1--22:18. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2023

    work page 2023

  3. [3]

    Learning probabilistic termination proofs

    Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Learning probabilistic termination proofs. In CAV (2) , volume 12760 of Lecture Notes in Computer Science , pages 3--26. Springer, 2021

    work page 2021

  4. [4]

    Quantitative automata model checking of autonomous stochastic hybrid systems

    Alessandro Abate, Joost - Pieter Katoen, and Alexandru Mereacre. Quantitative automata model checking of autonomous stochastic hybrid systems. In HSCC , pages 83--92. ACM , 2011

    work page 2011

  5. [5]

    Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems

    Alessandro Abate, Maria Prandini, John Lygeros, and Shankar Sastry. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica , 44(11):2724 -- 2734, 2008

    work page 2008

  6. [6]

    Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs

    Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotn \' y . Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang. , 2( POPL ):34:1--34:32, 2018

    work page 2018

  7. [7]

    Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs

    Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In SAS , volume 6337 of Lecture Notes in Computer Science , pages 117--133. Springer, 2010

    work page 2010

  8. [8]

    S. Axler. Measure, Integration & Real Analysis . Graduate Texts in Mathematics. Springer International Publishing, 2019

    work page 2019

Show all 52 references
  1. [9]

    Model checking probabilistic systems

    Christel Baier, Luca de Alfaro, Vojtech Forejt, and Marta Kwiatkowska. Model checking probabilistic systems. In Handbook of Model Checking , pages 963--999. Springer, 2018

    2018

  2. [10]

    Haverkort, Holger Hermanns, and Joost - Pieter Katoen

    Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost - Pieter Katoen. Performance evaluation and model checking join forces. Commun. ACM , 53(9):76--85, 2010

    2010

  3. [11]

    Principles of model checking

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

    2008

  4. [12]

    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. In CAV (1) , volume 13371 of Lecture Notes in Computer Science , pages 33--54. Springer, 2022

    2022

  5. [13]

    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. In TACAS (2) , volume 13994 of Lecture Notes in Computer Science , pages 41...

    2023

  6. [14]

    D. P. Bertsekas and S. E. Shreve. Stochastic optimal control: T he discrete-time case . Athena Scientific, 1996

    1996

  7. [15]

    Probabilistic program analysis with martingales

    Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with martingales. In CAV , volume 8044 of Lecture Notes in Computer Science , pages 511--526. Springer, 2013

    2013

  8. [16]

    Neural Lyapunov control

    Ya - Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov control. In NeurIPS , pages 3240--3249, 2019

    2019

  9. [17]

    Termination analysis of probabilistic programs through positivstellensatz's

    Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. Termination analysis of probabilistic programs through positivstellensatz's. In CAV (1) , volume 9779 of Lecture Notes in Computer Science , pages 3--22. Springer, 2016

    2016

  10. [18]

    Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs

    Krishnendu Chatterjee, Hongfei Fu, Petr Novotn \' y , and Rouzbeh Hasheminezhad. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst. , 40(2):7:1--7:45, 2018

    2018

  11. [19]

    Sound and complete certificates for quantitative termination analysis of probabilistic programs

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and or e Z ikeli\' c . Sound and complete certificates for quantitative termination analysis of probabilistic programs. In CAV (1) , volume 13371 of Lecture Notes in Computer Science , pages 55--78. Springer, 2022

    2022

  12. [20]

    Henzinger, Mathias Lechner, and or e Z ikeli\' c

    Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, and or e Z ikeli\' c . A learner-verifier framework for neural network controllers and certificates of stochastic systems. In TACAS (1) , volume 13993 of Lecture Notes in Computer Science , pages 3--25. Springer, 2023

    2023

  13. [21]

    Stochastic invariants for probabilistic termination

    Krishnendu Chatterjee, Petr Novotn \' y , and or e Z ikeli\' c . Stochastic invariants for probabilistic termination. In POPL , pages 145--160. ACM , 2017

    2017

  14. [22]

    Semantics of probabilistic programming: A gentle introduction

    Fredrik Dahlqvist and Alexandra Silva. Semantics of probabilistic programming: A gentle introduction. In Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva, editors, Foundations of Probabilistic Programming , pages 1--42. Cambridge University Press, 2020

    2020

  15. [23]

    Leonardo Mendon c a de Moura and Nikolaj S. Bj rner. Z3: an efficient SMT solver. In TACAS , volume 4963 of Lecture Notes in Computer Science , pages 337--340. Springer, 2008

    2008

  16. [24]

    Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu

    Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Quantitative multi-objective verification for probabilistic systems. In TACAS , volume 6605 of Lecture Notes in Computer Science , pages 112--127. Springer, 2011

    2011

  17. [25]

    Termination of nondeterministic probabilistic programs

    Hongfei Fu and Krishnendu Chatterjee. Termination of nondeterministic probabilistic programs. In VMCAI , volume 11388 of LNCS , pages 468--490. Springer, 2019

    2019

  18. [26]

    Timon Gehr, Sasa Misailovic, and Martin T. Vechev. PSI: exact symbolic inference for probabilistic programs. In CAV (1) , volume 9779 of Lecture Notes in Computer Science , pages 62--83. Springer, 2016

    2016

  19. [27]

    Timon Gehr, Samuel Steffen, and Martin T. Vechev. \( \)PSI : exact inference for higher-order probabilistic programs. In PLDI , pages 883--897. ACM , 2020

    2020

  20. [28]

    Neural termination analysis

    Mirco Giacobbe, Daniel Kroening, and Julian Parsert. Neural termination analysis. In ESEC/SIGSOFT FSE , pages 633--645. ACM , 2022

    2022

  21. [29]

    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

  22. [30]

    Hern \'a ndez-Lerma and J

    O. Hern \'a ndez-Lerma and J. B. Lasserre. Discrete-time M arkov control processes , volume 30 of Applications of Mathematics . Springer-Verlag, 1996

    1996

  23. [31]

    Modular verification for almost-sure termination of probabilistic programs

    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

    2019

  24. [32]

    Kallenberg

    O. Kallenberg. Foundations of modern probability . Springer Science & Business Media, 2006

    2006

  25. [33]

    Semantics of probabilistic programs

    Dexter Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci. , 22(3):328--350, 1981

    1981

  26. [34]

    Kwiatkowska

    Marta Z. Kwiatkowska. Quantitative verification: models techniques and tools. In ESEC/SIGSOFT FSE , pages 449--458. ACM , 2007

    2007

  27. [35]

    Kwiatkowska, Gethin Norman, and David Parker

    Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Quantitative analysis with the probabilistic model checker PRISM . In QAPL , volume 153 of Electronic Notes in Theoretical Computer Science , pages 5--31. Elsevier, 2005

    2005

  28. [36]

    Henzinger

    Mathias Lechner, or e Z ikeli\' c , Krishnendu Chatterjee, and Thomas A. Henzinger. Stability verification in stochastic control systems via neural network supermartingales. In AAAI , pages 7326--7336. AAAI Press, 2022

    2022

  29. [37]

    Safety certification for stochastic systems via neural barrier functions

    Frederik Baymler Mathiesen, Simeon Craig Calvert, and Luca Laurenti. Safety certification for stochastic systems via neural barrier functions. IEEE Control. Syst. Lett. , 7:973--978, 2023

    2023

  30. [38]

    Games, probability and the quantitative \( \) -calculus qm \( \)

    Annabelle McIver and Carroll Morgan. Games, probability and the quantitative \( \) -calculus qm \( \) . In LPAR , volume 2514 of Lecture Notes in Computer Science , pages 292--310. Springer, 2002

    2002

  31. [39]

    Abstraction, Refinement and Proof for Probabilistic Systems

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

    2005

  32. [40]

    Tweedie, and Peter W

    Sean Meyn, Richard L. Tweedie, and Peter W. Glynn. Markov Chains and Stochastic Stability . Cambridge Mathematical Library. Cambridge University Press, 2 edition, 2009

    2009

  33. [41]

    Probabilistic predicate transformers

    Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. , 18(3):325--353, 1996

    1996

  34. [42]

    Bounded expectations: resource analysis for probabilistic programs

    Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. Bounded expectations: resource analysis for probabilistic programs. In PLDI , pages 496--512. ACM , 2018

    2018

  35. [43]

    Automated and formal synthesis of neural barrier certificates for dynamical models

    Andrea Peruffo, Daniele Ahmed, and Alessandro Abate. Automated and formal synthesis of neural barrier certificates for dynamical models. In TACAS (1) , volume 12651 of Lecture Notes in Computer Science , pages 370--388. Springer, 2021

    2021

  36. [44]

    A User's Guide to Measure Theoretic Probability

    David Pollard. A User's Guide to Measure Theoretic Probability . Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, 2001

    2001

  37. [45]

    Royden and P

    H.L. Royden and P. Fitzpatrick. Real Analysis . Prentice Hall, 4 edition, 2010

    2010

  38. [46]

    Program Synthesis by Sketching

    Armando Solar-Lezama . Program Synthesis by Sketching . PhD thesis, University of California at Berkeley, USA , 2008

    2008

  39. [47]

    Seshia, and Vijay A

    Armando Solar - Lezama, Liviu Tancau, Rastislav Bod \' k, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS , pages 404--415. ACM , 2006

    2006

  40. [48]

    Ranking and repulsing supermartingales for reachability in randomized programs

    Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst. , 43(2):5:1--5:46, 2021

    2021

  41. [49]

    Quantitative model-checking of controlled discrete-time markov processes

    Ilya Tkachev, Alexandru Mereacre, Joost - Pieter Katoen, and Alessandro Abate. Quantitative model-checking of controlled discrete-time markov processes. Inf. Comput. , 253:1--35, 2017

    2017

  42. [50]

    Towards quantitative verification of probabilistic transition systems

    Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic transition systems. In ICALP , volume 2076 of Lecture Notes in Computer Science , pages 421--432. Springer, 2001

  43. [51]

    Di Wang, Jan Hoffmann, and Thomas W. Reps. Central moment analysis for cost accumulators in probabilistic programs. In PLDI , pages 559--573. ACM , 2021

    2021

  44. [52]

    Cost analysis of nondeterministic probabilistic programs

    Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. Cost analysis of nondeterministic probabilistic programs. In PLDI , pages 204--220. ACM , 2019

    2019

Pith tools

Reviewed May 24, 2026 · model on record in the stance chip above.