IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series > 2018 > Resource Morphisms for Specifying Concurrent Programs in Separation Logic: An Introduction
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Ignacio Fábregas

jueves 29 de noviembre de 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.