Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Two-variable separation logic and its inner circle
Demri S., Deters M. ACM Transactions on Computational Logic16 (2):1-36,2015.Type:Article
Date Reviewed: Jun 23 2015

Separation logic, an extension of Hoare logic, is currently a very active area of research. This paper investigates the expressiveness of this logic by exploring various restricted forms of it. Relations between fragments of separation logic and related logics are also studied, and via translations the relationships between these logics are expressed.

The introduction of the paper explains known results, describes the results that are derived in the following sections, and gives a map showing the relationships between the various logics.

The following sections introduce some restricted form of separation logic where formulas contain only one record field and a finite number of bounded variables. Next, some formulas often used in the following sections are defined and an encoding of data words via these formulas is presented. The kind of heaps used in this encoding, called fishbone heaps, are used a lot throughout the remainder of the paper. Finally, the section is concluded by the presentation of a new special variant modal logic for describing heaps. Section 3 builds on the previous section by further advancing the technical terms and constructing a translation from the propositional temporal interval logic into separation logic with two quantified variables and without the so-called “magic wand” operator. The possibility of this translation yields that separation logic with two quantified variables is decidable but not elementary recursive. The fourth section finally proves that the satisfiability problem of the separation logic with two bounded variables and the “magic wand” operator is not decidable. This is achieved by encoding Minsky machines and reducing the halting problem. A conclusion wraps up the results and points out some research directions.

The paper contains a lot of technical tricks, which are nevertheless presented in a way that is very intuitively graspable. The intuition of fishbone heaps and the depiction of their structure are very helpful. On the whole, I consider this a very enjoyable paper.

Reviewer:  Markus Wolf Review #: CR143549 (1509-0800)
Bookmark and Share
 
Specifying And Verifying And Reasoning About Programs (F.3.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Specifying And Verifying And Reasoning About Programs": Date
Programming: the derivation of algorithms
Kaldewaij A., Prentice-Hall, Inc., Upper Saddle River, NJ, 1990. Type: Book (9780132041089)
Aug 1 1991
An introduction to programming with specifications
Kubiak R., Rudziński R., Sokolowski S., Academic Press Prof., Inc., San Diego, CA, 1991. Type: Book (9780124276208)
Jun 1 1992
Observational implementation of algebraic specifications
Hennicker R. Acta Informatica 28(3): 187-230, 1991. Type: Article
Jul 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy