h1

000780877 001__ 780877
000780877 005__ 20251023115709.0
000780877 0247_ $$2HBZ$$aHT020344010
000780877 0247_ $$2Laufende Nummer$$a38925
000780877 0247_ $$2datacite_doi$$a10.18154/RWTH-2020-00940
000780877 037__ $$aRWTH-2020-00940
000780877 041__ $$aEnglish
000780877 082__ $$a004
000780877 1001_ $$0P:(DE-82)IDM01605$$aMatheja, Christoph$$b0$$urwth
000780877 245__ $$aAutomated reasoning and randomization in separation logic$$cvorgelegt von Christoph Matheja, M.Sc.$$honline
000780877 260__ $$aAachen$$c2020
000780877 300__ $$a1 Online-Ressource (x, 504 Seiten) : Illustrationen, Diagramme
000780877 3367_ $$02$$2EndNote$$aThesis
000780877 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000780877 3367_ $$2BibTeX$$aPHDTHESIS
000780877 3367_ $$2DRIVER$$adoctoralThesis
000780877 3367_ $$2DataCite$$aOutput Types/Dissertation
000780877 3367_ $$2ORCID$$aDISSERTATION
000780877 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University
000780877 502__ $$aDissertation, RWTH Aachen University, 2020$$bDissertation$$cRWTH Aachen University$$d2020$$gFak01$$o2020-01-09
000780877 5203_ $$aWir 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.$$lger
000780877 520__ $$aWe 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.$$leng
000780877 588__ $$aDataset connected to Lobid/HBZ
000780877 591__ $$aGermany
000780877 653_7 $$aHoare logic
000780877 653_7 $$aabstraction
000780877 653_7 $$aautomated verification
000780877 653_7 $$aentailment checking
000780877 653_7 $$aformal methods
000780877 653_7 $$aprobabilistic programming
000780877 653_7 $$aprobabilistic programs
000780877 653_7 $$aprogram analysis
000780877 653_7 $$aquantitative separation logic
000780877 653_7 $$arandomized algorithms
000780877 653_7 $$aseparation logic
000780877 653_7 $$asymbolic execution
000780877 653_7 $$aweakest preconditions
000780877 653_7 $$aweakest preexpectations
000780877 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth
000780877 7001_ $$aIosif, Radu$$b2$$eThesis advisor
000780877 8564_ $$uhttps://publications.rwth-aachen.de/record/780877/files/780877.pdf$$yOpenAccess
000780877 8564_ $$uhttps://publications.rwth-aachen.de/record/780877/files/780877_source.zip$$yRestricted
000780877 8564_ $$uhttps://publications.rwth-aachen.de/record/780877/files/780877.gif?subformat=icon$$xicon$$yOpenAccess
000780877 8564_ $$uhttps://publications.rwth-aachen.de/record/780877/files/780877.jpg?subformat=icon-1440$$xicon-1440$$yOpenAccess
000780877 8564_ $$uhttps://publications.rwth-aachen.de/record/780877/files/780877.jpg?subformat=icon-180$$xicon-180$$yOpenAccess
000780877 8564_ $$uhttps://publications.rwth-aachen.de/record/780877/files/780877.jpg?subformat=icon-640$$xicon-640$$yOpenAccess
000780877 8564_ $$uhttps://publications.rwth-aachen.de/record/780877/files/780877.jpg?subformat=icon-700$$xicon-700$$yOpenAccess
000780877 909CO $$ooai:publications.rwth-aachen.de:780877$$pdnbdelivery$$pdriver$$pVDB$$popen_access$$popenaire
000780877 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM01605$$aRWTH Aachen$$b0$$kRWTH
000780877 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH
000780877 9141_ $$y2020
000780877 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000780877 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation)$$x0
000780877 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
000780877 961__ $$c2020-02-17T13:18:11.391108$$x2020-01-20T18:12:44.329921$$z2020-02-17T13:18:11.391108
000780877 9801_ $$aFullTexts
000780877 980__ $$aI:(DE-82)120000_20140620
000780877 980__ $$aI:(DE-82)121310_20140620
000780877 980__ $$aUNRESTRICTED
000780877 980__ $$aVDB
000780877 980__ $$aphd