Rybalchenko, Andrey (Prof. Dr.); Podelski, Andreas (Prof. Dr.)
Sprache:
en
Fachgebiet:
DAT Datenverarbeitung, Informatik
TU-Systematik:
DAT 500d
Kurzfassung:
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.
Übersetzte Kurzfassung:
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.