AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Saarbrücken

In concurrent verification, separation logic provides a rich theory for handling resources that are owned exclusively. However, the situation is more complicated for temporarily shared, read-only state, where resources might be shared and then later reclaimed exclusively. We believe that a framework for temporarily-shared, read-only state should meet two key goals not adequately met by prior techniques. One, it should allow and encourage users to introduce new logical mechanisms for temporary-sharing. Two, it should provide a logic for the manipulation of shared state in a way that is agnostic to the mechanism with which that state is shared, thereby enabling modularity.

In this talk, I will present Leaf, a library in the Iris separation logic which accomplishes both of these goals by introducing a novel operator, which we call guarding, that allows one proposition to represent a shared version of another. Guarding exhibits a composable theory of temporary sharing, meeting the above goals and supporting a variety of logical sharing mechanisms, including a formalism suitable for more automated verification frameworks.

---
Please contact the office team for Zoom details.

Annika Meiser

+49 681 9303 9105

--email hidden

Zoom

passcode not visible

logged in users only