MASTERÂ Assignment
Practical Probabilistic Program Verification
Type : Master M-CS
Period: December, 2024 - May, 2025
Student : Jaarsveld, F. van (Franka, Student M-CS)
Date Final project: May 21, 2025
Supervisors:
Abstract:
This thesis explores the practical verification of probabilistic programs using Caesar, a weakest preexpectation-based verification tool for reasoning about the expected behaviour of discrete probabilistic programs. The Bounded Retransmission Protocol (BRP) is studied as a case study. A key contribution of this work is the abstraction and decomposition of BRP into two geometric-like programs, enabling more effective reasoning about the protocol's behaviour and facilitating the stepwise verification strategy. Theoretical verification of key properties (positive almost-sure termination, success probability, and the expectation of the number of failed and sent transmissions) was largely successful using weakest preexpectation calculus. Translating these results into verification using Caesar introduced practical challenges, particularly in invariant discovery. Additionally, even valid invariants did not always lead to successful verification due to limitations in Caesar’s current implementation, particularly in SMT solver performance and the handling of exponentials. However, through workarounds including alternative invariants and a 'fueled' exponential function, meaningful properties of BRP were verified. This thesis demonstrates how such techniques support practical verification in Caesar and concludes with a discussion of its strengths, limitations, and recommendations for effective use.