Georgiou, P. (2019). Trace Reasoning for formal verification : guiding vampire in induction [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.71683
Automatisierte Softwareverifikation gewinnt durch die fortschreitende Digitalisierung zunehmend an Bedeutung. Unter diesem Licht widmet sich diese Masterarbeit der automatisierten Softwareverifikation mit Hilfe von automatisierten Beweissystemen in Prädikatenlogik. Insbesondere werden Programme mit Arrays und Schleifen hinsichtlich funktionaler Korrektheit für einfache, als auch relationale Spezifikationen untersucht. Vor allem werden relationale Eigenschaften typischerweise verwendet, um Sicherheits- und Datenschutzgarantien in Anwendungen der Systemsicherheit zu formulieren. Dies erfordert oftmals Quantorenalternierung. Für die Verifizierung dieser Eigenschaften werden imperative Programme auf ein Gültigkeits- problem in eine neue Logik, die sogenannte Trace Logic, reduziert. Durch Reasoningaktivitäten über natürliche und ganze Zahlen, erfordern automatisierte Beweise in dieser Logik auch induktive Schlüsse, die nur schwer automatisch vollzogen werden können. In diesem Sinne widmet sich diese Arbeit der Formulierung geeigneter Lemmata, genannt Trace Lemmas, die das automatische Beweissystem bei Schlüssen, die Induktion erfordern, leitet. Das Ziel der Arbeit ist es geeignete Sets an Trace Lemmas für verschiedene Eigenschaften zu definieren und zu formulieren, sodass automatisierte Beweise mit Hilfe des VAMPIRE-Beweissystems generiert werden können ohne von programmspezifischen Annotationen durch Experten abhängig zu sein.
de
This work is motivated by automating reasoning for program analysis and verification in full first-order logic. We are interested in reachability and relational properties about functional correctness of programs with loops and arrays. Particularly, relational properties are typically used to formulate security and privacy guarantees in applications of system security, and often require reasoning about first-order formulas with quantifier-alternations. In our approach, we reduce the verification task of reachability and relational properties of imperative programs to a validity problem into a new logic, called trace logic, that is an expressive instance of first-order logic. Properties in trace logic involve reasoning about natural numbers and integers, and thus impose the burden of automating inductive reasoning in the full first-order setting of theorem proving. We address this challenge by automatically instantiating a set of so-called trace lemmas that guide first-order provers in inductive reasoning. The aim of this thesis is to identify a "reasonable" set of sound trace lemmas that allow superposition-based automated theorem provers to prove inductive (non-)relational properties, without relying on user-provided program annotations like program-specific loop invariants. To discharge verification conditions we rely on the first-order theorem prover Vampire.