fixed point theory

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite …
PDF Cite DOI Artifact Evaluated
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Lower Bounds for Possibly Divergent Probabilistic Programs
We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to …
PDF Cite Slides DOI
Lower Bounds for Possibly Divergent Probabilistic Programs
Latticed $k$-Induction with an Application to Probabilistic Programs
We revisit two well-established verification techniques, $k$-induction and bounded model checking (BMC), in the more general setting of …
PDF Cite Slides DOI Artifact Evaluated Pulp Fiction
Latticed $k$-Induction with an Application to Probabilistic Programs