### Abstract

We bring the labelled sequent calculus $LS_{PASL}$ for propositional abstract separation logic to Isabelle. The tactics given here are directly applied on an extension of the Separation Algebra in the AFP. In addition to the cancellative separation algebra, we further consider some useful properties in the heap model of separation logic, such as indivisible unit, disjointness, and cross-split. The tactics are essentially a proof search procedure for the calculus $LS_{PASL}$. We wrap the tactics in an Isabelle method called separata, and give a few examples of separation logic formulae which are provable by separata.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics
- Tools

### Session Separata

- Separata

### Depends on

- Separation Algebra

### Auto-related entries

- Unbounded Separation Logic
- A Sequent Calculus Prover for First-Order Logic with Functions
- Verifying Imperative Programs using Auto2

## Cite

×

Separata-AFP

    @article{Separata-AFP,
      author  = {Zhe Hou and David Sanan and Alwen Tiu and Rajeev Gore and Ranald Clouston},
      title   = {Separata: Isabelle tactics for Separation Algebra},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Separata.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
- Nov 17, 2016 : Isabelle2016