Almost-sure termination (AST) is a fundamental property of probabilistic programs and essential for verifying the total correctness of randomized algorithms. Recent advances have established sound and relatively complete proof rules for AST at the level of probabilistic control-flow graphs (pCFGs). Applying these results to probabilistic programs, however, requires a formal translation to pCFGs and a proof that AST is preserved under this translation. In this thesis, we establish such a translation enabling the application of pCFG-based proof rules to probabilistic programs. Moreover, we introduce a new program-level proof rule for AST, based on distribution transformer semantics, which avoids syntactic complexity at the pCFG level and integrates naturally with existing verification frameworks for probabilistic programs. Using this rule, we provide new formal proofs for AST of the Fast Dice Roller and the Loaded Fast Dice Roller algorithms, complementing previous partial correctness results to total correctness proofs.
Jonas Seidel (Thu,) studied this question.