Search

This dissertation presents a formalization of ordinary differential equations (ODEs) and the verification of rigorous (with guaranteed error bounds) numerical algorithms in the interactive theorem prover Isabelle/HOL. The formalization comprises flow and Poincaré map of dynamical systems. The verified algorithms are based on Runge-Kutta methods and affine arithmetic. They certify numerical bounds for the Lorenz attractor and thereby lift the numerical part of Tucker's proof of Smale's 14th problem onto a formal foundation., Diese Dissertation stellt eine Formalisierung von gewöhnlichen Differentialgleichungen (GDGL) und die Verifikation von rigorosen (mit garantierten Fehlerschranken) numerischen Algorithmen im interaktiven Theorembeweiser Isabelle/HOL vor. Die Formalisierung umfasst Fluss und Poincaré-Abbildung dynamischer Systeme. Die verifizierten Algorithmen basieren auf Runge-Kutta-Verfahren und affiner Arithmetik. Sie zertifizieren numerische Schranken für den Lorenz Attraktor und heben dadurch den numerischen Teil von Tuckers Beweis von Smales 14. Problem auf eine formale Grundlage.

This thesis combines three formal verification techniques — theorem proving, satisfiability checking (runtime monitoring), and reachability analysis — for formally analysing autonomous vehicles. First, we formalise the required elements which will be the foundation for formally analysing autonomous vehicles. Next, we formalise a collection of selected traffic rules from the German traffic code (Straßenverkhersordnung) and propose a method to monitor them formally. Lastly, we demonstrate how to use reachability analysis to formally construct a manoeuvre automaton which can be used for motion planning of autonomous vehicles., Diese Dissertation kombiniert drei Techniken der formale Verifikation - Theorembeweisen, Erfüllbarkeitsanalyse der Aussagenlogik und Erreichbarkeitsanalyse - um autonome Fahrzeuge formal zu analysieren. Zuerst werden die notwendigen Elemente formalisiert, die als Grundlage zur formalen Analyse autonomer Fahrzeuge dienen. Weiterhin wurde eine Menge an ausgewählten Verkehrsregeln der Straßenverkehrsordnung formalisiert und eine Methode vorgeschlagen, die deren Einhaltung formal überwacht. Zuletzt wird die Verwendung von Erreichbarkeitsanalyse zur formalen Konstruktion eines Manöver-Automaten demonstriert, der zur Bewegungsplanung autonomer Fahrzeuge verwendet werden kann.

The Flow Framework from "Local Reasoning for Global Graph Properties" [Siddharth Krishna, ESOP 2020] introduces a separation algebra that allows handling potentially unbounded side-effects of modifications to global graph properties in a modular fashion. In this thesis we formalize the Flow Framework as presented in “Local Reasoning for Global Graph Properties”. Subsequently, we demonstrate the application of the Flow Framework by verifying a graph algorithm. Finally, we present a significantly refined proof for a central theorem of the framework.

In this thesis, we present a proof of the functional correctness of the Fibonacci heap decrease-key operation using a separation logic framework implemented for Imperative HOL, an imperative verification framework built on top of Isabelle/HOL. This is a follow-up on Daniel Stüwe’s Master’s thesis [17], where he verified all Fibonacci heap operations (most notably delete-min) except for decrease-key and delete, which require a handle to the element to be changed or removed, respectively. His approach is based on first verifying a functional version of the Fibonacci heap and then showing that the imperative implementation correctly models the functional one. Using an augmented version of his approach, which also works for decrease-key, turned out to be too complex. Thus, the decrease-key operation was proven with an alternative approach where the heap is modeled as a map from addresses to (abstract) heap nodes. Together with Daniel Stüwe’s thesis, this means that the complete functionality of the Fibonacci heap was verified, even though the two different approaches are not directly compatible. For that reason, we also proved the functional correctness of make-heap, heap-union, get-min, and of a function creating a heap with a single element with the help of the new approach.

This thesis combines three formal verification techniques — theorem proving, satisfiability checking (runtime monitoring), and reachability analysis — for formally analysing autonomous vehicles. First, we formalise the required elements which will be the foundation for formally analysing autonomous vehicles. Next, we formalise a collection of selected traffic rules from the German traffic code (Straßenverkhersordnung) and propose a method to monitor them formally. Lastly, we demonstrate how to use reachability analysis to formally construct a manoeuvre automaton which can be used for motion planning of autonomous vehicles., Diese Dissertation kombiniert drei Techniken der formale Verifikation - Theorembeweisen, Erfüllbarkeitsanalyse der Aussagenlogik und Erreichbarkeitsanalyse - um autonome Fahrzeuge formal zu analysieren. Zuerst werden die notwendigen Elemente formalisiert, die als Grundlage zur formalen Analyse autonomer Fahrzeuge dienen. Weiterhin wurde eine Menge an ausgewählten Verkehrsregeln der Straßenverkehrsordnung formalisiert und eine Methode vorgeschlagen, die deren Einhaltung formal überwacht. Zuletzt wird die Verwendung von Erreichbarkeitsanalyse zur formalen Konstruktion eines Manöver-Automaten demonstriert, der zur Bewegungsplanung autonomer Fahrzeuge verwendet werden kann.

Following the demand for increased proof automation in the interactive theorem prover Isabelle, this thesis describes how SMT solvers improve on the state of the art. Our main contributions are a sound translation from Isabelle's higher-order logic to the first-order logic of SMT solvers, and efficient checking of proofs found by the SMT solver Z3. Based on a large evaluation, we find that many theorems can now be proved automatically and almost instantaneously for which time-consuming user ingenuity was previously required. Checking Z3's proofs is fast thanks to our extensive optimizations. Further contributions are a new tool and methodology to verify the functional correctness of C code in conjunction with the automatic program verifier VCC. We demonstrate their suitability on real-world implementations of tree and graph algorithms., Der Nachfrage nach erhöhter Beweisautomatisierung für den interaktiven Theorembeweiser Isabelle folgend zeigt diese Arbeit, wie SMT-Löser den Stand der Technik verbessern können. Unsere Hauptbeiträge sind eine korrekte Übersetzung von Isabelles höherstufiger Logik in die erststufige Logik von SMT-Lösern sowie die effiziente Rekonstruktion von Beweisen des SMT-Lösers Z3. Mittels einer umfangreichen Evaluierung belegen wir, dass viele Theoreme nun automatisch und nahezu sofort bewiesen werden können, wofür Benutzer früher eingehend nachdenken mußten. Das Überprüfen von Z3-Beweisen ist dank unserer aufwendigen Optimierungen schnell. Weitere Beiträge sind ein neues Werkzeug und eine neue Methode, um funktionale Korrektheit von C-Code im Zusammenspiel mit dem automatischen Programmbeweiser VCC zu zeigen. Wir demonstrieren ihre Eignung für Implementierungen aus der Praxis anhand von Baum- und Graphalgorithmen.