Title: Automated Reasoning over Arrays in the Superposition Calculus
Language: English
Authors: Hochrainer, Christoph 
Qualification level: Diploma
Keywords: automated reasoning; program semantics; trace logic; invariants; first-order theorem proving
automated reasoning; program semantics; trace logic; invariants; first-order theorem proving
Advisor: Kovacs, Laura 
Issue Date: 2020
Number of Pages: 71
Qualification level: Diploma
Abstract: 
In den letzen Jahren gab es enorme Fortschritte im Bereich automatisierter Softwareverifikation und Programanalyse. Dennoch wurden einige Herausforderungen noch nicht vollständig bezwungen, sowie das automatisierte Verifizieren von unbeschrenkten Datenstrukturen, insbesondere Arrays, und Programme, die diese manipulieren. Indieser Arbeiter konzentrieren wir uns auf die Programmanalyse und -verifizierung in vollständiger Logik erster Ordnung. Diese Arbeit soll theoretische Grundlagen für die Automatisierung von Beweisen zu partieller Korrektheit für Eigenschaften über ganzzahlige Arrays in dem Superposition Calculus liefern. Besonders interessieren uns hierbei Eigenschaften mit verschiedenen Quantifizierungen: ∃, ∀ und ∀∃. Jede der ausgewählten Eigenschaften beschreibt bestimmte Programmverhaltensweisen, welche häufig in der Praxis anzutreffen sind und es ist daher wichtig diese zu beweisen. Als Grundlage für diese Arbeit verwenden wir die erst kürzlich vorgestellte Trace-Logik, eine Instanz der Logik erster Ordnung, und das Framework Rapid, welches die logische Codierung der Programme liefert. Durch Verwendung einer generischen Eigenschaft P, die eine Eigenschaft über Arrays darstellt, wurden die notwendigen Lemma und die Axiomatisierung der Trace-Logik verallgemeinert und es konnten allgemeinere Beweise erstellt werden. Diese können nun verwendet werden, um Beweis für eine konkretisierte Eigenschaft zu instanziieren. Mit den durch die Beweise gewonnenen Erkenntnissen sind wir nun in der Lage automatisierte Beweise der Eigenschaften in allgemeiner oder konkretisierter Form, mit Hilfe des Superposition-basiertem Theorembeweiser Vampire, durchzuführen.

Automated reasoning for program verification has made a lot of advancements in the past years. Nevertheless, one of the remaining challenges is automated reasoning over unbound data structures, in particular arrays, and programs manipulating them. In this thesis we will focus on program analysis and verification in full first-order logic.This work aims to provide theoretical basis to automate partial correctness proofs for software properties over integer arrays in the superposition calculus. Particularly, we are interested in properties of different quantifier settings: ∃, ∀ and ∀∃. Each of the chosen properties describe specific program behaviors that occur often in practice and are therefore important to prove. As foundation for this work we use the recently introduced trace logic, an instance of first-order logic and the framework Rapid, which provides the logical encoding of the programs. By using a generic property P, representing some property over arrays, we were able to generalize necessary lemmas and axiomatization of trace logic to produce more general proofs. These can be used to quickly instantiate a proof for a concrete property. With the insights gained throughout this work, we are now able to automate the proofs of the specific properties in general and concrete form, using the superposition-based theorem prover Vampire.
URI: https://doi.org/10.34726/hss.2020.77511
http://hdl.handle.net/20.500.12708/15173
DOI: 10.34726/hss.2020.77511
Library ID: AC15692227
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)

26
checked on Feb 18, 2021

Download(s)

12
checked on Feb 18, 2021

Google ScholarTM

Check


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