University of Twente Student Theses

Login

Practical Probabilistic Program Verification using Caesar

Jaarsveld, Franka van (2025) Practical Probabilistic Program Verification using Caesar.

[img] PDF
2MB
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.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:https://purl.utwente.nl/essays/106318
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page