First-order theorem proving for program analysis and theory reasoning

Abstract

In dieser Dissertation untersuchen wir, wie mit Beweismethoden der Prädikatenlogik erster Stufe Programmeigenschaften gefunden und bewiesen werden können. Die erarbeiteten Methoden wurden in einem vollständig automatisierten Tool namens Lingva umgesetzt, welches quantifizierte Invarianten über Arrays generiert. Wir zeigen experimentell, dass die generierten Invarianten das Verhalten der analysierten Schleifen zusammenfassen. Unsere Arbeit basiert auf der erst jüngst entwickelten Methode der Elimination von Symbolen bei Generierung von Invarianten, wobei ein sättigungsbasierter Beweiser für Theoreme der Prädikationlogik verwendet wird. Da Programmeigenschaften sowohl logische als auch arithmetische Operationen über unbeschränkte Datenstrukturen wie Arrays involvieren, sind für das Erzeugen und Beweisen von Programmeigenschaften effiziente Methoden für das Schlussfolgern in das Schlussfolgern in den Theorien und über den Quantoren notwendig. Ein weiterer Beitrag dieser Arbeit ist die Erweiterung des prädikatenlogikbasierten Theorembeweisers Vampire um Schrankenausbreitungsmethoden zur Lösung von Systemen linearer Ungleichungen. Somit kann Vampire als automatisches Tool zum Entscheiden der Erfüllbarkeit von Ungleichungssytemen auf der Menge der rationalen Zahlen oder reellen Zahlen verwendet werden. Wir zeigen experimentell, dass die Effizient der Schrankenausbreitung in Vampire im Vergleich mit state-of-the-art Satisfiability Modulo Theory Lösern auf schweren linearen Optimierungsproblemen gut abschneidet. Unser arithmetischer Löser ist auf Konjunktionen linearer Ungleichungen limitiert. Jedoch haben arithmetische Programmeigenschaften üblicherweise eine komplexere boolesche Struktur aus Kombinationen von Konjunktionen, Disjunktionen und Negierungen. Um daher unsere Arbeit auf komplexe arithmetische Eigenschaften anwendbar zu machen, wurden booleschen Entscheidungsproblem (SAT) Löser in Vampire integriert. Unsere Arbeit nutzt das kürzlich entwickelte AVATAR Framework um das Schlussfolgerungen über Theoreme der Prädikatenlogik von der booleschen Struktur der Probleme zu trennen. Wir beschreiben die technischen und implementierungsbezogenen Herausforderungen die bei der Integration der effizientesten SAT Lösern in Vampire auftreten und verwenden unsere Implementierung zur Evaluierung des AVATAR Frameworks mit einer Vielzahl von Problemen der TPTP Bibliothek automatisierter Theorembeweiser.

In this thesis we study the use of first-order theorem proving for generating and proving program properties. Our thesis provides a fully automated tool support, called Lingva, for generating quantified invariants of programs over arrays, and shows experimentally that the generated invariants summarize the behavior of the considered loops. Our work is based on the recently introduced symbol elimination method for invariant generation, using a saturation-based first-order theorem prover. As program properties involve both logical and arithmetical operations over unbounded data structures, such as arrays, generating and proving program properties requires efficient methods for reasoning with both theories and quantifiers. Another contribution of this thesis comes with the integration of the bound propagation method for solving systems of linear inequalities in the first-order theorem prover Vampire. Our work provides an automated tool support for using Vampire for deciding satisfiability of a system of linear inequalities over the reals or rationals. We experimentally show that bound propagation in Vampire performs well when compared to state-of-the-art satisfiability modulo theory solvers on hard linear optimization problems. Our arithmetic solver is limited to conjunction of linear inequalities, while arithmetic program properties usually have a more complex boolean structure, using a combination of logical conjunction, disjunction and negation. To make our work applicable for handling such complex arithmetic properties, another contribution of this thesis is the integration of boolean satisfiability (SAT) solvers within Vampire. Our work exploits the recently introduced AVATAR framework for separating the first-order reasoning part of a problem from its boolean structure. We describe our technical and implementation challenges for integrating the best performing SAT solvers within Vampire, and use our implementation to evaluate the AVATAR framework on a large set of problems coming from the TPTP library of automated theorem provers.