Campus Event Calendar
Event Entry
What and Who
Inductive Reasoning in Separation Logic
Nicolas Peltier
Laboratory of Informatics of Grenoble
Talk
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 29 January 2025
10:30
60 Minutes
E1 4
024
Saarbrücken
Abstract
Separation Logic (SL) is a foundational tool in program verification,
designed to simplify reasoning about dynamically allocated memory. A
central challenge in this domain involves testing entailments between SL
formulas. In this talk, I will present recent advancements in addressing
the entailment problem in SL, in the presence of inductively defined
predicate symbols. I will provide an overview of key results on the
decidability and complexity of this problem across various SL fragments.
Subsequently, I will delve into an inductive proof procedure that is
sound, complete, and terminating for a specific fragment of inductive
definitions. To conclude, I will outline ongoing and future research
directions in this area.
designed to simplify reasoning about dynamically allocated memory. A
central challenge in this domain involves testing entailments between SL
formulas. In this talk, I will present recent advancements in addressing
the entailment problem in SL, in the presence of inductively defined
predicate symbols. I will provide an overview of key results on the
decidability and complexity of this problem across various SL fragments.
Subsequently, I will delve into an inductive proof procedure that is
sound, complete, and terminating for a specific fragment of inductive
definitions. To conclude, I will outline ongoing and future research
directions in this area.
Contact
Jennifer Müller
+49 681 9325 2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 01/22/2025 12:08
Jennifer Müller, 01/20/2025 15:21 -- Created document.
Jennifer Müller, 01/20/2025 15:21 -- Created document.