Title: Trace Reasoning for formal verification : guiding vampire in induction
Language: English
Authors: Georgiou, Pamina 
Qualification level: Diploma
Advisor: Kovács, Laura
Issue Date: 2019
Number of Pages: 58
Qualification level: Diploma
Abstract: 
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.

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.
Keywords: formal methods; software verification; system security; automated reasoning; first-order theorem proving
formal methods; software verification; system security; automated reasoning; first-order theorem proving
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-131509
http://hdl.handle.net/20.500.12708/11483
Library ID: AC15530600
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

24
checked on Jun 16, 2021

Download(s)

47
checked on Jun 16, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.