guest ::
Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning = Korrekte und vollständige Beweisregeln für fast sichere Terminierung: von probabilistischen Kontrollflussgraphen zur Beweisführung auf Programmebene
2026
Masterarbeit, RWTH Aachen University, 2026
Veröffentlicht auf dem Publikationsserver der RWTH Aachen University
Genehmigende Fakultät
Fak09
Hauptberichter/Gutachter
; ;
Tag der mündlichen Prüfung/Habilitation
2026-03-31
Online
DOI: 10.18154/RWTH-2026-04488
URL: http://publications.rwth-aachen.de/record/1034043/files/1034043.pdf
Einrichtungen
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
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.
OpenAccess: 
PDF
Dokumenttyp
Master Thesis
Format
online
Sprache
English
Interne Identnummern
RWTH-2026-04488
Datensatz-ID: 1034043
Beteiligte Länder
Germany
|
The record appears in these collections: |
PDF