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
Copyright Status
Unknown
Socpus ID
85047432624 (Scopus)
Source API URL
https://api.elsevier.com/content/abstract/scopus_id/85047432624
STARS Citation
Bao, Yuyan; Leavens, Gary T.; and Ernst, Gidon, "Unifying Separation Logic And Region Logic To Allow Interoperability" (2018). Scopus Export 2015-2019. 9683.
https://stars.library.ucf.edu/scopus2015/9683