h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

Automated reasoning and randomization in separation logic



Verantwortlichkeitsangabevorgelegt von Christoph Matheja, M.Sc.

ImpressumAachen 2020

Umfang1 Online-Ressource (x, 504 Seiten) : Illustrationen, Diagramme


Dissertation, RWTH Aachen University, 2020

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University


Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
;

Tag der mündlichen Prüfung/Habilitation
2020-01-09

Online
DOI: 10.18154/RWTH-2020-00940
URL: https://publications.rwth-aachen.de/record/780877/files/780877.pdf

Einrichtungen

  1. Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) (121310)
  2. Fachgruppe Informatik (120000)

Inhaltliche Beschreibung (Schlagwörter)
Hoare logic (frei) ; abstraction (frei) ; automated verification (frei) ; entailment checking (frei) ; formal methods (frei) ; probabilistic programming (frei) ; probabilistic programs (frei) ; program analysis (frei) ; quantitative separation logic (frei) ; randomized algorithms (frei) ; separation logic (frei) ; symbolic execution (frei) ; weakest preconditions (frei) ; weakest preexpectations (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Wir studieren drei Aspekte der Programmverifikation mit Separation Logic (SL):1. Die Analyse quantitativer Eigenschaften, wie z.B. die Wahrscheinlichkeit der Terminierung ohne Speicherfehler, von probabilistischen Programmen.2. Die automatisierte Analyse der Robustheit von und Implikationsbeziehungen zwischen Formeln im symbolischen Heap-Fragment von Separation Logic.3. Die automatisierte Analyse von Zeigerprogrammen durch Kombination von SL-basierten Abstraktionen mit den obigen Techniken und Model Checking. Bezüglich des ersten Punktes erweitern wir SL zu einer quantitativen Separation Logic (QSL) zur Analyse von Quantitäten, die zu reellen Zahlen ausgewertet werden, anstelle von Prädikaten, die zu Wahrheitswerten ausgewertet werden. Auf Grundlage von QSL entwickeln wir ein Kalkül der schwächsten Vorbedingungen à la Dijkstra, der praktisch alle klassichen Eigenschaften beibehält. Wir zeigen, dass dieser Kalkül eine korrekte und konservative Erweiterung sowohl von SL als auch der schwächsten Vorerwartungen von McIver and Morgan ist. Wir demonstrieren seine Anwendbarkeit anhand mehrerer Fallstudien. Bezüglich des zweiten Punktes entwickeln wir ein algorithmisches Grundgerüst auf Basis von Heap-Automaten um Robustheitseigenschaften, z.B. Erfüllbarkeit oder Azyklizität, von symbolischen Heaps mit induktiven Definitionen nachzuweisen. Wir betrachten zwei Ansätze um Implikationen in Fragmenten von SL zu zeigen. Dies umfasst einen Algorithmus für Implikationen zwischen grafischen symbolischen Heaps, der in nichtdeterministischer Polynomialzeit läuft. Bezüglich des dritten Punktes, stellen wir Attestor vor - ein Werkzeug zur automatisierten Analyse von Java Programmen, die mit dynamischen Datenstrukturen arbeiten. Dies beinhaltet die Generierung eines abstrakten Zustandsraumes unter Verwendung induktiver Definitionen in SL. Eigenschaften einzelner Zustände werden durch Heap-Automaten beschrieben. Ein Model Checker ermöglicht dann die Verifikation von struktureller und funktionaler Korrektheit. Attestor ist vollautomatisch, modular und liefert aussagekräftiges visuelles Feedback inklusive Gegenbeispielen falls die Verifikation fehlschlägt.

We study three aspects of program verification with separation logic:1. Reasoning about quantitative properties, such as the probability of memory-safe termination, of randomized heap-manipulating programs.2. Automated reasoning about the robustness of and entailments between formulas in the symbolic heap fragment of separation logic itself.3. Automated reasoning about pointer programs by combining abstractions based on separation logic with the above techniques and model checking. Regarding the first item, we extend separation logic to reason about quantities, which evaluate to real numbers, instead of predicates, which evaluate to Boolean values. Based on the resulting quantitative separation logic, we develop a weakest precondition calculus à la Dijkstra for quantitative reasoning about randomized heap-manipulating programs. We show that this calculus is a sound and conservative extension of both separation logic and McIver and Morgan's weakest preexpectations which preserves virtually all properties of classical separation logic. We demonstrate its applicability by several case studies. Regarding the second item, we develop an algorithmic framework based on heap automata to compositionally check robustness properties, e.g., satisfiability or acyclicity, of symbolic heaps with inductive predicate definitions. We consider two approaches to discharge entailments for fragments of separation logic. In particular, this includes a pragmatic decision procedure with nondeterministic polynomial-time complexity for entailments between graphical symbolic heaps. Regarding the third item, we introduce Attestor - an automated verification tool for analyzing Java programs operating on dynamic data structures. The tool involves the generation of an abstract state space employing inductive predicate definitions in separation logic. Properties of individual states are defined by heap automata. LTL model checking is then applied to this state space, supporting the verification of both structural and functional correctness properties. Attestor is fully automated, procedure modular, and provides informative visual feedback including counterexamples for violated properties.

OpenAccess:
Download fulltext PDF
(additional files)

Dokumenttyp
Dissertation / PhD Thesis

Format
online

Sprache
English

Externe Identnummern
HBZ: HT020344010

Interne Identnummern
RWTH-2020-00940
Datensatz-ID: 780877

Beteiligte Länder
Germany

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > Department of Computer Science
Publication server / Open Access
Public records
Publications database
120000
121310

 Record created 2020-01-20, last modified 2023-04-08


OpenAccess:
Download fulltext PDF
(additional files)
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)