Informatik und Informationswissenschaft

Deductive verification of probabilistic programs via independence and conditioning

Time
Wednesday, 19. June 2024
13:30 - 15:00

Location
R 611

Organizer
Tobias Sutter

Speaker:
Emanuele D'Osualdo

This event is part of an event series „Fachbereichskolloquium“.

Abstract:
 

In this talk I will outline the main conceptual breakthroughs provided by Separation Logic, a successful framework to reason about programs with rigorous logics. Starting from a simple observation about the shortcomings of Hoare logic to reason about heap-manipulating programs, the concept of “separation” provided a new tool for thought that proved to be extremely useful beyond the initial application.

After a brief overview of Separation Logic, I will present the main ideas behind my Bluebell project, which proposes a new Separation Logic that can reason about probabilistic behaviour.

back