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.