guest ::
| 001 | 780877 | ||
| 005 | 20251023115709.0 | ||
| 024 | 7 | _ | |2 HBZ |a HT020344010 |
| 024 | 7 | _ | |2 Laufende Nummer |a 38925 |
| 024 | 7 | _ | |2 datacite_doi |a 10.18154/RWTH-2020-00940 |
| 037 | _ | _ | |a RWTH-2020-00940 |
| 041 | _ | _ | |a English |
| 082 | _ | _ | |a 004 |
| 100 | 1 | _ | |0 P:(DE-82)IDM01605 |a Matheja, Christoph |b 0 |u rwth |
| 245 | _ | _ | |a Automated reasoning and randomization in separation logic |c vorgelegt von Christoph Matheja, M.Sc. |h online |
| 260 | _ | _ | |a Aachen |c 2020 |
| 300 | _ | _ | |a 1 Online-Ressource (x, 504 Seiten) : Illustrationen, Diagramme |
| 336 | 7 | _ | |0 2 |2 EndNote |a Thesis |
| 336 | 7 | _ | |0 PUB:(DE-HGF)11 |2 PUB:(DE-HGF) |a Dissertation / PhD Thesis |b phd |m phd |
| 336 | 7 | _ | |2 BibTeX |a PHDTHESIS |
| 336 | 7 | _ | |2 DRIVER |a doctoralThesis |
| 336 | 7 | _ | |2 DataCite |a Output Types/Dissertation |
| 336 | 7 | _ | |2 ORCID |a DISSERTATION |
| 500 | _ | _ | |a Veröffentlicht auf dem Publikationsserver der RWTH Aachen University |
| 502 | _ | _ | |a Dissertation, RWTH Aachen University, 2020 |b Dissertation |c RWTH Aachen University |d 2020 |g Fak01 |o 2020-01-09 |
| 520 | 3 | _ | |a 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. |l ger |
| 520 | _ | _ | |a 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. |l eng |
| 588 | _ | _ | |a Dataset connected to Lobid/HBZ |
| 591 | _ | _ | |a Germany |
| 653 | _ | 7 | |a Hoare logic |
| 653 | _ | 7 | |a abstraction |
| 653 | _ | 7 | |a automated verification |
| 653 | _ | 7 | |a entailment checking |
| 653 | _ | 7 | |a formal methods |
| 653 | _ | 7 | |a probabilistic programming |
| 653 | _ | 7 | |a probabilistic programs |
| 653 | _ | 7 | |a program analysis |
| 653 | _ | 7 | |a quantitative separation logic |
| 653 | _ | 7 | |a randomized algorithms |
| 653 | _ | 7 | |a separation logic |
| 653 | _ | 7 | |a symbolic execution |
| 653 | _ | 7 | |a weakest preconditions |
| 653 | _ | 7 | |a weakest preexpectations |
| 700 | 1 | _ | |0 P:(DE-82)IDM00048 |a Katoen, Joost-Pieter |b 1 |e Thesis advisor |u rwth |
| 700 | 1 | _ | |a Iosif, Radu |b 2 |e Thesis advisor |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/780877/files/780877.pdf |y OpenAccess |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/780877/files/780877_source.zip |y Restricted |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/780877/files/780877.gif?subformat=icon |x icon |y OpenAccess |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/780877/files/780877.jpg?subformat=icon-1440 |x icon-1440 |y OpenAccess |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/780877/files/780877.jpg?subformat=icon-180 |x icon-180 |y OpenAccess |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/780877/files/780877.jpg?subformat=icon-640 |x icon-640 |y OpenAccess |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/780877/files/780877.jpg?subformat=icon-700 |x icon-700 |y OpenAccess |
| 909 | C | O | |o oai:publications.rwth-aachen.de:780877 |p openaire |p open_access |p VDB |p driver |p dnbdelivery |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)IDM01605 |a RWTH Aachen |b 0 |k RWTH |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)IDM00048 |a RWTH Aachen |b 1 |k RWTH |
| 914 | 1 | _ | |y 2020 |
| 915 | _ | _ | |0 StatID:(DE-HGF)0510 |2 StatID |a OpenAccess |
| 920 | 1 | _ | |0 I:(DE-82)121310_20140620 |k 121310 |l Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) |x 0 |
| 920 | 1 | _ | |0 I:(DE-82)120000_20140620 |k 120000 |l Fachgruppe Informatik |x 1 |
| 980 | 1 | _ | |a FullTexts |
| 980 | _ | _ | |a I:(DE-82)120000_20140620 |
| 980 | _ | _ | |a I:(DE-82)121310_20140620 |
| 980 | _ | _ | |a UNRESTRICTED |
| 980 | _ | _ | |a VDB |
| 980 | _ | _ | |a phd |
| Library | Collection | CLSMajor | CLSMinor | Language | Author |
|---|