DC FieldValueLanguage
dc.contributor.advisorZuleger, Florian-
dc.contributor.authorPagel, Jens-
dc.date.accessioned2020-12-01T08:39:32Z-
dc.date.issued2020-
dc.date.submitted2020-11-
dc.identifier.citation<div class="csl-bib-body"> <div class="csl-entry">Pagel, J. (2020). <i>Decision procedures for separation logic: beyond symbolic heaps</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.85941</div> </div>-
dc.identifier.urihttps://doi.org/10.34726/hss.2020.85941-
dc.identifier.urihttp://hdl.handle.net/20.500.12708/16333-
dc.description.abstractSeparation 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.en
dc.formatxxv, 240 Seiten-
dc.languageEnglish-
dc.language.isoen-
dc.subjectseparation logicen
dc.subjectprogram logicsen
dc.subjectsoftware verificationen
dc.subjectdecision proceduresen
dc.subjectautomated reasoningen
dc.subjectinductive definitionsen
dc.subjectlocal reasoningen
dc.subjectmodularityen
dc.titleDecision procedures for separation logic: beyond symbolic heapsen
dc.typeThesisen
dc.typeHochschulschriftde
dc.identifier.doi10.34726/hss.2020.85941-
dc.publisher.placeWien-
tuw.thesisinformationTechnische Universität Wien-
tuw.publication.orgunitE192 - Institut für Logic and Computation-
dc.type.qualificationlevelDoctoral-
dc.identifier.libraryidAC16084902-
dc.description.numberOfPages240-
dc.thesistypeDissertationde
dc.thesistypeDissertationen
item.languageiso639-1en-
item.cerifentitytypePublications-
item.cerifentitytypePublications-
item.openaccessfulltextOpen Access-
item.openairetypeThesis-
item.openairetypeHochschulschrift-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.grantfulltextopen-
item.fulltextwith Fulltext-
Appears in Collections:Thesis

Files in this item:


Page view(s)

344
checked on Jan 19, 2022

Download(s)

202
checked on Jan 19, 2022

Google ScholarTM

Check


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