# Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations

## TL;DR

This paper introduces resource morphisms and simulations in separation logic, enabling the adaptation of verified concurrent programs across different resource models for improved proof reuse.

## Contribution

It presents a novel concept of resource morphisms and integrates them into separation logic, enhancing modularity and reusability of proofs in concurrent program verification.

## Key findings

- Resource morphisms preserve resource structure.
- Morphisms enable compositionally adapting programs to different resources.
- Enhanced proof reuse in concurrent program verification.

## Abstract

In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources---a form of state transition system---to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of resource morphism, i.e. structure-preserving function on resources, and show how to effectively integrate it into separation logic, using an associated notion of morphism-specific simulation. We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.

---
Source: https://tomesphere.com/paper/1904.07136