Dynamic Separation Logic
Electronic Notes in Theoretical Informatics and Computer Science, vol. Volume 3 - Proceedings of...
Abstract
This paper introduces a dynamic logic extension of separation logic. The assertion language of separation logic is extended with modalities for the five types of the basic instructions of separation logic: simple assignment, look-up, mutation, allocation, and de-allocation. The main novelty of the resulting dynamic logic is that it allows to combine different approaches to resolving these modalities. One such approach is based on the standard weakest precondition calculus of separation logic. The other approach introduced in this paper provides a novel alternative formalization in the proposed dynamic logic extension of separation logic. The soundness and completeness of this axiomatization has been formalized in the Coq theorem prover.
Authors 3
-
Frank S. de Boer Aachen
Leiden University · Centrum Wiskunde & Informatica
Affiliation as printed
Computer Security group Centrum Wiskunde & Informatica (CWI) Amsterdam , the Netherlands
Leiden Institute for Advanced Computer Science (LIACS) Leiden University Leiden , the Netherlands
Computer Security group Centrum Wiskunde & Informatica (CWI) Amsterdam, the Netherlands
Leiden Institute for Advanced Computer Science (LIACS) Leiden University Leiden, the Netherlands
-
Hans-Dieter A. Hiep Aachen
Leiden University · Centrum Wiskunde & Informatica
Affiliation as printed
Computer Security group Centrum Wiskunde & Informatica (CWI) Amsterdam , the Netherlands
Leiden Institute for Advanced Computer Science (LIACS) Leiden University Leiden , the Netherlands
Computer Security group Centrum Wiskunde & Informatica (CWI) Amsterdam, the Netherlands
Leiden Institute for Advanced Computer Science (LIACS) Leiden University Leiden, the Netherlands
-
Open University of the Netherlands
Affiliation as printed
Department of Computer Science Open University (OU) Heerlen , the Netherlands
Department of Computer Science Open University (OU) Heerlen, the Netherlands
Cited by 1 stored of 1
1 result
No patents citing this paper on Lens.org (checked 2026-10-11).