Title: Decision Procedures for Separation Logic: Beyond Symbolic Heaps
Other Titles: null
Language: English
Authors: Pagel, Jens 
Qualification level: Doctoral
Keywords: separation logic; program logics; software verification; decision procedures; automated reasoning; inductive definitions; local reasoning; modularity
Advisor: Zuleger, Florian 
Issue Date: 2020
Number of Pages: 240
Qualification level: Doctoral
Separation logic is a formalism for the verification of programs that make ex- tensive 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 un- bounded size. SSLdata also is the first decidable separation logic that com- bines 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 decid- ability 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.
URI: https://doi.org/10.34726/hss.2020.85941
DOI: 10.34726/hss.2020.85941
Library ID: AC16084902
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

checked on Feb 25, 2021


checked on Feb 25, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.