Computability and Complexity Results for a Spatial Assertion Language for Data Structures

Abstract. This paper studies a recently developed an approach to reasoning about mutable data structures, which uses an assertion language with spatial conjunction and implication connectives. We investigate computability and complexity properties of a subset of the language, which allows statements about the shape of pointer structures (such as “there is a link from x to y”) to be made, but not statements about the data held in cells (such as “x is a prime number”). We show that validity, even for this restricted language, is not r.e., but that the quantifierfree sublanguage is decidable. We then consider the complexity of model checking and validity for several fragments.

• Type: Conference
• Year: 2001
• Where: FSTTCS
• Authors: Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn
• Keywords: Assertion Language, FSTTCS 2001, Implication Connectives, Mutable Data Structures, Software Engineering