Deductive verification of probabilistic programs via independence and conditioning
Wann
Mittwoch, 19. Juni 2024
13:30 bis 15 Uhr
Wo
R 611
Veranstaltet von
Tobias Sutter
Vortragende Person/Vortragende Personen:
Emanuele D'Osualdo
Diese Veranstaltung ist Teil der Veranstaltungsreihe „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.
