Decision procedures for separation logic: beyond symbolic heaps

Abstract

Separation logic is a formalism for the verification of programs that make extensive use of dynamic resources, such as heap-allocated memory. Separation logic enables modular program analyses and correctness proofs through its key innovation, the separating conjunction. This has sparked the development of mature, scalable static analysis and verification tools in both academia and industry. The degree of automation and the precision that such tools can achieve depend on the availability of solvers for checking the satisfiability and entailment problems for separation-logic formulas. As these problems are undecidable in general, various decidable fragments of separation logic have been proposed. This leads to a trade-off between expressiveness and tractability: On the one hand, we need solvers for expressive fragments of separation logic to be able to automatically prove interesting properties or discover subtle bugs. On the other hand, increasing the expressiveness of a logical formalism generally comes at a computational cost. In this thesis, I focus on two variants of separation logic that attempt to strike the balance between expressiveness and tractability. 1. I introduce a new separation logic, strong-separation logic with lists, trees, and data, SSLdata. This logic combines a nonstandard semantics of the separating conjunction with a novel approach for constraining the data stored within data structures. This enables automated reasoning about the functional correctness of programs that use lists and trees of unbounded size. SSLdata also is the first decidable separation logic that combines unbounded data structures with the so-called magic wand operator. This makes it possible, for example, to implement weakest-precondition calculi using SSLdata. I present a PSpace decision procedure for the logic with magic wand but without constraints on data and an SMT-based, coNP decision procedure for the entailment problem of a fragment of SSLdata that subsumes the widely-used symbolic-heap fragment. 2. I design a novel decision procedure for a variant of separation logic with inductive definitions (SLID). SLID supports the definition of custom pred- icates by recursive equation systems. This makes it possible to reason about intricate overlaid data structures, such as trees with linked leaves (used to implement sorted-set data structures). While the entailment problem for SLID is undecidable in general, a large fragment was shown to be decidable by Iosif et al. [?]. The original decidability proof relied on a reduction that caused a blow-up of the problem size by several exponentials. In contrast, the decision procedure I present in this thesis is asymptotically optimal and operates directly on SLID formulas.