Automated reasoning over Arrays in the superposition calculus

Abstract

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.

In den letzten Jahren gab es enorme Fortschritte im Bereich automatisierter Softwareverifikation und Programmanalyse. Dennoch wurden einige Herausforderungen noch nicht vollständig bezwungen, sowie das automatisierte Verifizieren von unbeschränkten Datenstrukturen, insbesondere Arrays, und Programme, die diese manipulieren. In dieser 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.