Expectation Invariants for Probabilistic Program Loops as Fixed Points
No abstract available.
Related papers
- Data-Driven Invariant Learning for Probabilistic Programs CAV 2022
- Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time POPL 2020
- Mora - Automatic Generation of Moment-Based Invariants TACAS 2020
- Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops ESOP 2026
- Fixed Point Certificates for Reachability and Expected Rewards in MDPs TACAS 2025
- Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning PLDI 2023
- Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back OOPSLA 2025
- Invariant Generation for Multi-Path Loops with Polynomial Assignments VMCAI 2018