### Abstract

We present a generic type class implementation of separation algebra for Isabelle/HOL as well as lemmas and generic tactics which can be used directly for any instantiation of the type class.

The ex directory contains example instantiations that include structures such as a heap or virtual memory.

The abstract separation algebra is based upon "Abstract Separation Logic" by Calcagno et al. These theories are also the basis of the ITP 2012 rough diamond "Mechanised Separation Algebra" by the authors.

The aim of this work is to support and significantly reduce the effort for future separation logic developments in Isabelle/HOL by factoring out the part of separation logic that can be treated abstractly once and for all. This includes developing typical default rule sets for reasoning as well as automated tactic support for separation logic.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Session Separation_Algebra

- Separation_Algebra
- Sep_Heap_Instance
- Sep_Tactics
- Simple_Separation_Example
- Sep_Tactics_Test
- Map_Extra
- VM_Example
- Separation_Algebra_Alt
- Sep_Eq
- Types_D
- Abstract_Separation_D
- Separation_D

### Used by

- A Formal CHERI-C Memory Model
- Hoare Logics for Time Bounds
- Separata: Isabelle tactics for Separation Algebra

## Cite

×

Separation_Algebra-AFP

    @article{Separation_Algebra-AFP,
      author  = {Gerwin Klein and Rafal Kolanski and Andrew Boyton},
      title   = {Separation Algebra},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Separation_Algebra.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- May 11, 2012 : Isabelle2011-1