Abstract: Probabilistic programs are programs that feature probabilistic sampling statements. Their formal analysis is not only relevant to understand and verify randomized algorithms, but also to understand more general probabilistic models that can be represented by probabilistic programs. Our goal is to automate the verification of probabilistic programs, with a focus on approaches based on so-called weakest pre-expectations. The various existing calculi allow reasoning about expected values, expected run-times, reachability probabilities and more. We propose a quantitative intermediate verification language (HeyVL) and an associated quantitative assertion language (HeyLo) as a unified interface to encode verification problems using these various calculi. With our implementation, we contribute the first automated verification of a number of probabilistic programs.

Short Bio: Philipp is a PhD student at RWTH Aachen University in the group of Joost-Pieter Katoen. He is interested in formal semantics of probabilistic programs and taking their automated verification to the next level. Philipp has worked on the automation of proof techniques such as probabilistic IC3 (PrIC3) and probabilistic k-induction (kipro2) and is now building a more general verification infrastructure for probabilistic programs.

Organiza: Federico Olmedo, académico DCC.

--

Comunicaciones DCC