IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2018 > Resource Morphisms for Specifying Concurrent Programs in Separation Logic: An Introduction

Ignacio Fábregas

Thursday, November 29, 2018

10:45am Meeting room 302 (Mountain View), level 3

Ignacio Fábregas, Post-doctoral Researcher, IMDEA Software Institute

Resource Morphisms for Specifying Concurrent Programs in Separation Logic: An Introduction

Abstract:

In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources, i.e., state transition systems, to describe the invariants on the state and their allowed atomic changes. One of this logical frameworks is FCSL, developed by Aleksandar Nanevski et al. As usual, once we have a mathematical structure, it is only natural to study the functions that preserve them. This motivates the interest of defining and studying a morphism between resources. In this talk we will give an introduction to the main concepts of FCSL and the notion of resource morphism. We will also show how to apply morphisms to facilitate proof reuse between resources.