research-article

On probabilistic termination of functional programs with continuous distributions

Authors:

Luke OngAuthors Info & Claims

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 1312 - 1326

https://doi.org/10.1145/3453483.3454111

Published: 18 June 2021 Publication History

Abstract

We study termination of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions. Reasoning about the termination probability of programs with continuous distributions is hard, because the enumeration of terminating executions cannot provide any non-trivial bounds. We present a new operational semantics based on traces of intervals, which is sound and complete with respect to the standard sampling-based semantics, in which (countable) enumeration can provide arbitrarily tight lower bounds. Consequently we obtain the first proof that deciding almost-sure termination (AST) for programs with continuous distributions is Π₂⁰-complete (for CbN). We also provide a compositional representation of our semantics in terms of an intersection type system. In the second part, we present a method of proving AST for non-affine programs, i.e., recursive programs that can, during the evaluation of the recursive body, make multiple recursive calls (of a first-order function) from distinct call sites. Unlike in a deterministic language, the number of recursion call sites has direct consequences on the termination probability. Our framework supports a proof system that can verify AST for programs that are well beyond the scope of existing methods. We have constructed prototype implementations of our methods for computing lower bounds on the termination probability, and AST verification.

References

[1]

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

Digital Library

[2]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press. isbn:978-0-262-02649-9

Digital Library

[3]

Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics, Vol. 103). North-Holland. isbn:978-0-444-86748-3

[4]

Raven Beutner and Luke Ong. 2021. On Probabilistic Termination of Functional Programs with Continuous Distributions. CoRR, abs/2104.04990 (2021), arxiv:2104.04990. arxiv:2104.04990

[5]

Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul A. Szerlip, Paul Horsfall, and Noah D. Goodman. 2019. Pyro: Deep Universal Probabilistic Programming. J. Mach. Learn. Res., 20 (2019), 28:1–28:6. http://jmlr.org/papers/v20/18-403.html

[6]

Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. 2016. A lambda-calculus foundation for universal probabilistic programming. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. ACM, 33–46. https://doi.org/10.1145/2951913.2951942

Digital Library

[7]

Tomás Brázdil, Václav Brozek, Kousha Etessami, Antonín Kucera, and Dominik Wojtczak. 2010. One-Counter Markov Decision Processes. In Proceedings of the Twenty-First Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2010, Austin, Texas, USA, January 17-19, 2010. SIAM, 863–874. https://doi.org/10.1137/1.9781611973075.70

[8]

Tomás Brázdil, Javier Esparza, Stefan Kiefer, and Antonín Kucera. 2013. Analyzing probabilistic pushdown automata. Formal Methods Syst. Des., 43, 2 (2013), 124–163. https://doi.org/10.1007/s10703-012-0166-0

Digital Library

[9]

Flavien Breuvart and Ugo Dal Lago. 2018. On Intersection Types and Probabilistic Lambda Calculi. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018. ACM, 8:1–8:13. https://doi.org/10.1145/3236950.3236968

Digital Library

[10]

Benno Büeler, Andreas Enge, and Komei Fukuda. 2000. Exact Volume Computation for Polytopes: A Practical Study. Birkhäuser Basel, Basel. 131–154. isbn:978-3-0348-8438-9 https://doi.org/10.1007/978-3-0348-8438-9_6

[11]

Michael G. Burke. 1990. An Interval-Based Approach to Exhaustive and Incremental Interprocedural Data-Flow Analysis. ACM Trans. Program. Lang. Syst., 12, 3 (1990), 341–395. https://doi.org/10.1145/78969.78963

Digital Library

[12]

Bob Carpenter, Andrew Gelman, Matthew D. Hoffman, Daniel Lee, Ben Goodrich, Michael Betancourt, Marcus Brubaker, Jiqiang Guo, Peter Li, and Allen Riddell. 2017. Stan: A Probabilistic Programming Language. Journal of Statistical Software, Articles, 76, 1 (2017), 1–32. issn:1548-7660 https://doi.org/10.18637/jss.v076.i01

[13]

Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 8044). Springer, 511–526. https://doi.org/10.1007/978-3-642-39799-8_34

[14]

Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz’s. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 9779). Springer, 3–22. https://doi.org/10.1007/978-3-319-41528-4_1

[15]

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

Digital Library

[16]

Krishnendu Chatterjee, Petr Novotný, and Dorde Zikelic. 2017. Stochastic invariants for probabilistic termination. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. ACM, 145–160. http://dl.acm.org/citation.cfm?id=3009873

Digital Library

[17]

Jianhui Chen and Fei He. 2020. Proving almost-sure termination by omega-regular decomposition. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020. ACM, 869–882. https://doi.org/10.1145/3385412.3386002

Digital Library

[18]

Marco F. Cusumano-Towner, Feras A. Saad, Alexander K. Lew, and Vikash K. Mansinghka. 2019. Gen: a general-purpose probabilistic programming system with programmable inference. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. ACM, 221–236. https://doi.org/10.1145/3314221.3314642

Digital Library

[19]

Martin E. Dyer and Alan M. Frieze. 1988. On the Complexity of Computing the Volume of a Polyhedron. SIAM J. Comput., 17, 5 (1988), 967–974. https://doi.org/10.1137/0217060

Digital Library

[20]

Thomas Ehrhard, Michele Pagani, and Christine Tasson. 2018. Full Abstraction for Probabilistic PCF. J. ACM, 65, 4 (2018), 23:1–23:44. https://doi.org/10.1145/3164540

Digital Library

[21]

Thomas Ehrhard, Christine Tasson, and Michele Pagani. 2014. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014. ACM, 309–320. https://doi.org/10.1145/2535838.2535865

Digital Library

[22]

Kousha Etessami and Mihalis Yannakakis. 2009. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM, 56, 1 (2009), 1:1–1:66. https://doi.org/10.1145/1462153.1462154

Digital Library

[23]

Luis María Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic Termination: Soundness, Completeness, and Compositionality. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. ACM, 489–501. https://doi.org/10.1145/2676726.2677001

Digital Library

[24]

Hong Ge, Kai Xu, and Zoubin Ghahramani. 2018. Turing: A Language for Flexible Probabilistic Inference. In Proceedings of the Twenty-First International Conference on Artificial Intelligence and Statistics (Proceedings of Machine Learning Research, Vol. 84). PMLR, 1682–1690. http://proceedings.mlr.press/v84/ge18b.html

[25]

Noah D. Goodman, Vikash K. Mansinghka, Daniel M. Roy, Keith Bonawitz, and Joshua B. Tenenbaum. 2008. Church: a language for generative models. In UAI 2008, Proceedings of the 24th Conference in Uncertainty in Artificial Intelligence, Helsinki, Finland, July 9-12, 2008. AUAI Press, 220–229. https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=1346&proceeding_id=24

Digital Library

[26]

Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. 2014. Probabilistic programming. In Proceedings of the on Future of Software Engineering, FOSE 2014, Hyderabad, India, May 31 - June 7, 2014. ACM, 167–181. https://doi.org/10.1145/2593882.2593900

Digital Library

[27]

Mingzhang Huang, Hongfei Fu, and Krishnendu Chatterjee. 2018. New Approaches for Almost-Sure Termination of Probabilistic Programs. In Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11275). Springer, 181–201. https://doi.org/10.1007/978-3-030-02768-1_11

[28]

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

Digital Library

[29]

Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2015. On the Hardness of Almost-Sure Termination. In Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 9234). Springer, 307–318. https://doi.org/10.1007/978-3-662-48057-1_24

[30]

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

Digital Library

[31]

Andrew Kenyon-Roberts and Luke Ong. 2021. Supermartingales, Ranking Functions and Probabilistic Lambda Calculus. In 36nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. IEEE Computer Society.

[32]

S. C. Kleene. 1955. Hierarchies of number-theoretic predicates. Bull. Amer. Math. Soc., 61 (1955), 05, 193–213. https://doi.org/10.1090/S0002-9904-1955-09896-3

[33]

Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. 2019. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. IEEE, 1–14. https://doi.org/10.1109/LICS.2019.8785679

[34]

Dexter Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. Syst. Sci., 22, 3 (1981), 328–350. https://doi.org/10.1016/0022-0000(81)90036-2

[35]

Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca. 2021. Intersection types and (positive) almost-sure termination. Proc. ACM Program. Lang., 5, POPL (2021), 1–32. https://doi.org/10.1145/3434313

Digital Library

[36]

Ugo Dal Lago and Charles Grellois. 2019. Probabilistic Termination by Monadic Affine Sized Typing. ACM Trans. Program. Lang. Syst., 41, 2 (2019), 10:1–10:65. https://doi.org/10.1145/3293605

Digital Library

[37]

Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Informatics Appl., 46, 3 (2012), 413–450. https://doi.org/10.1051/ita/2012012

[38]

Jean B Lasserre. 1983. An analytical expression and an algorithm for the volume of a convex polyhedron in R^n. Journal of optimization theory and applications, 39, 3 (1983), 363–377.

[39]

Wonyeol Lee, Hangyeol Yu, and Hongseok Yang. 2018. Reparameterization Gradient for Non-differentiable Models. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada. 5558–5568. https://proceedings.neurips.cc/paper/2018/hash/b096577e264d1ebd6b41041f392eec23-Abstract.html

[40]

Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K. Mansinghka. 2020. Trace types and denotational semantics for sound programmable inference in probabilistic languages. Proc. ACM Program. Lang., 4, POPL (2020), 19:1–19:32. https://doi.org/10.1145/3371087

Digital Library

[41]

Carol Mak, C.-H. Luke Ong, Hugo Paquet, and Dominik Wagner. 2021. Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere. In Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings (Lecture Notes in Computer Science, Vol. 12648). Springer, 432–461. https://doi.org/10.1007/978-3-030-72019-3_16

Digital Library

[42]

Vikash K. Mansinghka, Daniel Selsam, and Yura N. Perov. 2014. Venture: a higher-order probabilistic programming platform with programmable inference. CoRR, abs/1404.0099 (2014), arxiv:1404.0099. arxiv:1404.0099

[43]

Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer. isbn:978-0-387-40115-7 https://doi.org/10.1007/b138392

[44]

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

Digital Library

[45]

Sean Meyn and Richard L. Tweedie. 2009. Markov Chains and Stochastic Stability (2nd ed.). Cambridge University Press.

Digital Library

[46]

Michael Mitzenmacher and Eli Upfal. 2005. Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press. isbn:978-0-521-83540-4 https://doi.org/10.1017/CBO9780511813603

Digital Library

[47]

Ramon E. Moore, R. Baker Kearfott, and Michael J. Cloud. 2009. Introduction to Interval Analysis. SIAM. isbn:978-0-89871-669-6 https://doi.org/10.1137/1.9780898717716

[48]

R. Motwani and P. Raghavan. 1995. Randomized algorithms. Cambridge University Press.

[49]

Akihiko Nishimura, David B Dunson, and Jianfeng Lu. 2020. Discontinuous Hamiltonian Monte Carlo for discrete parameters and discontinuous likelihoods. Biometrika, 107, 2 (2020), 365–380.

[50]

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. ACM, 672–681. https://doi.org/10.1145/2933575.2935317

Digital Library

[51]

Gordon D. Plotkin. 1977. LCF Considered as a Programming Language. Theor. Comput. Sci., 5, 3 (1977), 223–255. https://doi.org/10.1016/0304-3975(77)90044-5

[52]

M. O. Rabin. 1976. Probabilistic algorithms. In Algorithms and complexity: new directions and results. Academic Press, New York, 21–39.

[53]

Tom Rainforth. 2017. Automating Inference, Learning, and Design Using Probabilistic Programming. Ph.D. Dissertation. University of Oxford.

[54]

Reuven Y. Rubinstein and Dirk P. Kroese. 2017. Simulation and the Monte Carlo Method (3rd ed.). Wiley.

[55]

Eugene S. Santos. 1969. Probabilistic Turing Machines and Computability. Proc. Amer. Math. Soc., 22, 3 (1969), 704–710. issn:00029939, 10886826 http://www.jstor.org/stable/2037463

[56]

David Tolpin, Jan-Willem van de Meent, and Frank D. Wood. 2015. Probabilistic Programming in Anglican. In Machine Learning and Knowledge Discovery in Databases - European Conference, ECML PKDD 2015, Porto, Portugal, September 7-11, 2015, Proceedings, Part III (Lecture Notes in Computer Science, Vol. 9286). Springer, 308–311. https://doi.org/10.1007/978-3-319-23461-8_36

Digital Library

[57]

Dustin Tran, Alp Kucukelbir, Adji B. Dieng, Maja R. Rudolph, Dawen Liang, and David M. Blei. 2016. Edward: A library for probabilistic modeling, inference, and criticism. CoRR, abs/1610.09787 (2016), arxiv:1610.09787. arxiv:1610.09787

[58]

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

[59]

Yuan Zhou, Bradley J. Gram-Hansen, Tobias Kohn, Tom Rainforth, Hongseok Yang, and Frank Wood. 2019. LF-PPL: A Low-Level First Order Probabilistic Programming Language for Non-Differentiable Models. In The 22nd International Conference on Artificial Intelligence and Statistics, AISTATS 2019, 16-18 April 2019, Naha, Okinawa, Japan (Proceedings of Machine Learning Research, Vol. 89). PMLR, 148–157. http://proceedings.mlr.press/v89/zhou19b.html

Cited By

Kura SUnno H(2024)Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type SystemProceedings of the ACM on Programming Languages10.1145/36746628:ICFP(973-1002)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674662
Chatterjee KGoharshady AMeggendorfer TŽikelić Đ(2024)Quantitative Bounds on Resource Usage of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36498248:OOPSLA1(362-391)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649824
Majumdar RSathiyanarayana V(2024)Positive Almost-Sure Termination: Complexity and Proof RulesProceedings of the ACM on Programming Languages10.1145/36328798:POPL(1089-1117)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632879
Show More Cited By

Index Terms

On probabilistic termination of functional programs with continuous distributions
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
      2. Program verification
    2. Program semantics
      1. Operational semantics

Recommendations

Modular verification for almost-sure termination of probabilistic programs

In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as their theoretical ...
Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs

Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem asks ...
Stochastic invariants for probabilistic termination
POPL '17

Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2021

1341 pages

ISBN:9781450383912

DOI:10.1145/3453483

General Chair:
Stephen N. Freund
Williams College, USA
,
Program Chair:
Eran Yahav
Technion, Israel

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

PLDI '21

Sponsor:

SIGPLAN

PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 20 - 25, 2021

Virtual, Canada

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
182
Total Downloads

Downloads (Last 12 months)38
Downloads (Last 6 weeks)3

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kura SUnno H(2024)Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type SystemProceedings of the ACM on Programming Languages10.1145/36746628:ICFP(973-1002)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674662
Chatterjee KGoharshady AMeggendorfer TŽikelić Đ(2024)Quantitative Bounds on Resource Usage of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36498248:OOPSLA1(362-391)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649824
Majumdar RSathiyanarayana V(2024)Positive Almost-Sure Termination: Complexity and Proof RulesProceedings of the ACM on Programming Languages10.1145/36328798:POPL(1089-1117)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632879
Kassing JGiesl J(2023)Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency PairsAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_20(344-364)Online publication date: 1-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-38499-8_20
Chatterjee KGoharshady AMeggendorfer TŽikelić Đ(2022)Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic ProgramsComputer Aided Verification10.1007/978-3-031-13185-1_4(55-78)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_4
Kenyon-Roberts AOng CGorla D(2021)Supermartingales, ranking functions and probabilistic lambda calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470550(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470550

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents