### Expectation-Based Reasoning

Our approach is based on *weakest precondition-style reasoning*, generalized to probabilistic programs. We can reason about lower and upper bounds of expected values.

### A Quantitative Intermediate Verification Language

Caesar is built on our novel quantitative intermediate verification language *HeyVL*.

See our OOPSLA '23 paper!

### A Collaborative Effort

Caesar is an open-source project from RWTH Aachen University (MOVES group), Saarland University (QUAVE group), Denmark Technical University (SSE section), and University College London (PPLV group).

## Features of HeyVL โ Lossy List Traversal Example

Let's look at a program that traverses a list but has a chance of crashing during the traversal. We'll verify that the crash probability is at least 50% if the list has length 1.

We explain more of the details as part of our getting started guide.

### ๐ฅ `lossy_list`

Procedure

This procedure is the entry point. It has one output, the resulting list `l`

. In the body of `lossy_list`

, we traverse the list by repeatedly removing the first element using `pop`

. We model a 50% chance of crashing by a coin flip (`flip(0.5)`

) leading to `assert [false]`

.

`proc lossy_list(init_l: List) -> (l: List)`

pre [len(init_l) == 1] * 0.5 // quantitative specification!

post [true]

{

l = init_l

@invariant(exp(0.5, len(l)))

while len(l) > 0 {

var prob_choice: Bool = flip(0.5) // coin flip

if prob_choice {

l = pop(l) // next list element

} else {

assert [false] // crash

}

}

}

### ๐ Reading The Spec

Let's focus on the *quantitative specification* of `lossy_list`

:

`pre [len(init_l) == 1] * 0.5`

post [true]

The `post`

says that we are looking at the expected value of `[true]`

(i.e. 1) in the final states of the program. In other words, we are interested in the probability of running without an error.

The `pre`

specifies a lower bound to the probability of a run without crashing (expected value of the post `[true]`

). It says that if the length of the list is 1, then the lower bound is `0.5`

and otherwise `0`

.

To verify the spec, the `while`

loop has an `@invariant`

annotation with a probabilistic invariant.

### ๐ Axiomatizing Exponentials and Lists

Here is a strength of deductive verification: users can axomatize additional functions and data types that can be used for verification! We simply declare the uninterpreted sort and functions with just the necessary axioms in HeyVL.

`domain Exponentials {`

func exp(base: UReal, exponent: UInt): EUReal

axiom exp_base forall base: UReal.

exp(base, 0) == 1

axiom exp_step forall base: UReal, exponent: UInt.

exp(base, exponent + 1) == base * exp(base, exponent)

}

domain List {

func len(l: List): UInt

func pop(l: List): List

axiom list_len forall l: List.

len(pop(l)) == len(l) - 1

}

### ๐ Running Caesar

Download and extract the latest `caesar`

binary (or visit *Getting Started* for alternative installation options).

The example from above is included in the Git repository. After downloading and storing it in `examples/lossy_list.heyvl`

you can try Caesar on it:

`caesar examples/lossy_list.heyvl`

Caesar will print: `examples/lossy_list.heyvl: Verified.`