Title: Eine Entscheidungsprozedur für Separation-Logic mit Daten
Other Titles: A decision procedure for a separation logic with data
Language: English
Authors: Krulj, Stefan 
Qualification level: Diploma
Advisor: Weissenbacher, Georg 
Assisting Advisor: Pagel, Jens 
Issue Date: 2020
Number of Pages: 94
Qualification level: Diploma
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.

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.
Keywords: Separation Logik; SMT; Satisfiability Modulo Theory; Formale Verifikation
Separation Logic; SMT; Satisfiability Modulo Theories; Formal verification
URI: https://doi.org/10.34726/hss.2020.59461
http://hdl.handle.net/20.500.12708/16175
DOI: 10.34726/hss.2020.59461
Library ID: AC16071892
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

26
checked on Jun 18, 2021

Download(s)

30
checked on Jun 18, 2021

Google ScholarTM

Check


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