<div class="csl-bib-body">
<div class="csl-entry">Krulj, S. (2020). <i>Eine Entscheidungsprozedur für Separation-Logic mit Daten</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.59461</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2020.59461
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/16175
-
dc.description.abstract
Separation Logic (zu Deutsch etwa "Trennungslogik") ist eine Erweiterung des Hoare-Kalküls, welche logische Schlussfolgerungen über imperative Computer-Programme, die dynamische Heap-Speicher verwenden, erlaubt. Es ist ein beliebter Formalismus für Programme, welche dynamische Ressourcen manipulieren und wird bereits industriell eingesetzt. Die große Ausdruckskraft der Separation Logic erlaubt es modular komplizierte Konzepte, wie dynamisch allokierte Arrays, uneingeschränkte Zeigerarithmetik und rekursive Prozeduren abzubilden. SL_data* ist ein Fragment der Separation Logic, die auf einen Kompromiss zwischen Ausdruckskraft und Komplexität abzielt und ermöglicht Aussagen über im Heap-Speicher gespeicherte Daten zu treffen. Dabei liegen das Erfüllbarkeits-Problem in NP und das Gültigkeits-Problem von Implikationen in coNP. SL_data* kann auf Theorien reduziert werden, welche in gängigen SMT-Solvern verfügbar sind, und zur Darstellung von Daten eine beliebige Theorie verwenden. Mit SLOTH existiert bereits eine Implementierung der Entscheidungsprozedur, diese ist jedoch noch eingeschränkt. SL_data* erlaubt das Auswählen einer Adress- sowie Datentheorie, was jedoch von SLOTH nicht unterstützt wird. Zusätzlich wurde SLOTH noch nicht auf Performance optimiert und die Entscheidungen für einige Probleminstanzen dauern sehr lange. Wir schlagen Optimierungen für die SL_data*-Entscheidungsprozedur vor. Zusätzlich haben wir die Entscheidungsprozedur sowie die Optimierungen implementiert und einige Einschränkungen von SLOTH überwunden. Die Prozedur wurde in Z3, einem gängigen SMT-Solver integriert. Wir zeigen, die Effektivität der Optimierungen mit einer empirischen Studie.
de
dc.description.abstract
Separation Logic is an extension of Hoare Logic that allows reasoning about imperative programs that use dynamic data structures. It is a popular formalism for programs that manipulate the heap and on top of that has been proven on an industrial scale. Its expressive power permits modular definitions of complex concepts like dynamically allocated arrays, unrestricted pointer arithmetic and recursive procedures and data structures. SL_data* is a Separation Logic fragment with emphasis on data constraints and decidability. It aims to strike a balance between expressibility and complexity, with satisfiability being decidable in NP and entailment in coNP. SL_data* can be encoded into theories supported by off-the-shelf SMT-solvers and can be combined with arbitrary data theories. While with SLOTH a decision procedure implementation exists, it is still limited. The theory allows for configurable location and data sorts, but is not supported by SLOTH. Moreover, SLOTH has not yet been optimised for performance and the decision of some specific instances takes a long time. We propose optimisations for the decision procedure of SL_data*. In addition, have implemented the decision procedure that overcomes some of the current limits of SLOTH and integrated it within Z3, a state-of-the-art SMT solver. We show the effectiveness of the proposed optimisations with empirical benchmarks.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Separation Logik
de
dc.subject
SMT
de
dc.subject
Satisfiability Modulo Theory
de
dc.subject
Formale Verifikation
de
dc.subject
Separation Logic
en
dc.subject
SMT
en
dc.subject
Satisfiability Modulo Theories
en
dc.subject
Formal verification
en
dc.title
Eine Entscheidungsprozedur für Separation-Logic mit Daten
en
dc.title.alternative
A decision procedure for a separation logic with data
de
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2020.59461
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Stefan Krulj
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Pagel, Jens
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Diploma
-
dc.identifier.libraryid
AC16071892
-
dc.description.numberOfPages
94
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
item.languageiso639-1
en
-
item.fulltext
with Fulltext
-
item.openaccessfulltext
Open Access
-
item.mimetype
application/pdf
-
item.openairetype
master thesis
-
item.grantfulltext
open
-
item.openairecristype
http://purl.org/coar/resource_type/c_bdcc
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E186 - Institut für Computergraphik und Algorithmen