Cardinalities in Software Verification

Freiherr von Gleissenthall, Klaus

Klaus Freiherr von Gleissenthall

If you experience problems opening the document, please try this link.

Original title:: Cardinalities in Software Verification
Translated title:: Kardinalitäten in der Software Verifikation
Author:: Freiherr von Gleissenthall, Klaus
Year:: 2016
Document type:: Dissertation
Faculty/School:: Fakultät für Informatik
Advisor:: Rybalchenko, Andrey (Prof. Dr.)
Referee:: Rybalchenko, Andrey (Prof. Dr.); Podelski, Andreas (Prof. Dr.)
Language:: en
Subject group:: DAT Datenverarbeitung, Informatik
TUM classification:: DAT 500d
Abstract:: Many verification tasks require reasoning about cardinalities. Unfortunately, today's technology does not support the verification of programs that require such reasoning very well. In this thesis, we present two methods for this task. We have implemented both techniques and demonstrate their practicality on a set of benchmarks from various applications including distributed algorithms and bounding information leakage through side channels.
Translated abstract:: Für viele Verifikationsaufgaben ist es unerlässlich die Anzahl der Elemente in einer Menge (das heißt deren Kardinalität) erfassen zu können. Leider wird diese Art der quantitativen Verifikation von derzeit existierenden Methoden nicht unterstützt. Aus diesem Grund entwickelt diese Dissertation zwei Methoden für diese Aufgabe. Wir haben beide Techniken implementiert und demonstrieren ihre Anwendbarkeit auf eine Reihe von Problemen.
WWW:: https://mediatum.ub.tum.de/?id=1293444
Date of submission:: 24.02.2016
Oral examination:: 15.09.2016
File size:: 577524 bytes
Pages:: 75
Urn (citeable URL):: https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20160915-1293444-1-7
Last change:: 08.05.2017
BibTeX