Frank S. de Boer ; Hans-Dieter A. Hiep ; Stijn de Gouw - Dynamic Separation Logic

entics:12297 - Electronic Notes in Theoretical Informatics and Computer Science, November 23, 2023, Volume 3 - Proceedings of MFPS XXXIX - https://doi.org/10.46298/entics.12297
Dynamic Separation LogicArticle

Authors: Frank S. de Boer ; Hans-Dieter A. Hiep ; Stijn de Gouw

    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.


    Volume: Volume 3 - Proceedings of MFPS XXXIX
    Published on: November 23, 2023
    Accepted on: October 16, 2023
    Submitted on: September 19, 2023
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 253 times.
    This article's PDF has been downloaded 117 times.