Unifying Separation Logic And Region Logic To Allow Interoperability

Keywords

Fine-grained region logic; Formal specification; Formal verification; Framing; Hoare logic; Separation logic; Shared mutable data; Unified fine-grained region logic (UFRL)

Abstract

Framing is important for specification and verification, especially in programs that mutate data structures with shared data, such as DAGs. Both separation logic and region logic are successful approaches to framing, with separation logic providing a concise way to reason about data structures that are disjoint, and region logic providing the ability to reason about framing for shared mutable data. In order to obtain the benefits of both logics for programs with shared mutable data, this paper unifies them into a single logic, which can encode both of them and allows them to interoperate. The new logic thus provides a way to reason about program modules specified in a mix of styles.

Publication Date

8-1-2018

Publication Title

Formal Aspects of Computing

Volume

30

Issue

3-4

Number of Pages

381-441

Document Type

Article

Personal Identifier

scopus

DOI Link

https://doi.org/10.1007/s00165-018-0455-5

Socpus ID

85047432624 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/85047432624

This document is currently not available here.

Share

COinS