Search

We verify algorithms and reference implementations using the proof assistant Isabelle. Firstly, we formalize an abstract, general, and extensible library for transition systems and automata. Secondly, we verify an ample set partial order reduction algorithm and integrate it into the CAVA model checker. Thirdly, we verify an algorithm for rank-based Büchi complementation and use it to implement a Büchi equivalence checker., Wir verifizieren Algorithmen und Referenzimplementierungen mit dem Beweisassistenten Isabelle. Erstens formalisieren wir eine abstrakte, generelle, und erweiterbare Bibliothek für Transitionssysteme und Automaten. Zweitens verifizieren wir einen Ample Set Partial Order Reduction Algorithmus und integrieren diesen in den CAVA Model Checker. Drittens verifizieren wir einen Algorithmus für Rang-basierte Büchi-Komplementierung und implementieren damit einen Büchi-Äquivalenzprüfer.

This thesis explores the adoption of two established specification patterns within the Rust verifier Creusot: type invariants and ghost code. Type invariants empower users to attach logical predicates to data types, which Creusot enforces for all values of a type. Ghost code enables auxiliary constructs that bolster verification without affecting the program's runtime behavior. Especially when employed in tandem, these patterns enhance the expressivity of specifications and ensure the scalability of Rust verification. We introduce an innovative framework for type invariants, including its implementation in Creusot. Moreover, we scrutinize Creusot's current implementation of ghost code, identifying soundness deficiencies and presenting refinements to address them. Our evaluation demonstrates that these extensions not only facilitate more concise program specifications but also maintain robust verifiability.

This thesis applies formal verification to the running time analysis of algorithms. First, three Hoare logics for time bounds from the literature are studied and their application to probabilistic programs is explored. Then, a practical framework using Separation Logic with Time Credits is presented. Finally, stepwise refinement is extended to reason about the resource usage of programs. The theory is applied to formally verify the running time of introspection sort and Kruskal‘s algorithm., Diese Dissertation wendet formale Verifikation auf die Laufzeitanalyse von Algorithmen an. Zuerst werden drei Hoare Logiken für Laufzeitschranken untersucht und ihre Anwendung auf probabilistische Programme erkundet. Dann wird ein konkretes Werkzeug basierend auf Separationslogik mit Time Credits realisiert und die Technik Schrittweise Verfeinerung auf Laufzeitanalyse erweitert. Mithilfe der entwickelten Werkzeuge wird die Laufzeitanalyse von Introsort und Kruskal‘s Algorithmus verifiziert.

This dissertation describes my work in the formalisation of mathematics with the proof assistant Isabelle/HOL, particularly mathematics related to asymptotic concepts such as limits and function growth. This work consists of both the formalisation of fundamental mathematical material for the Isabelle/HOL standard library and the creation of new proof automation tools. Both of these have since been used successfully in many formalisation applications both in pure mathematics (such as analysis and number theory) and computer science (i.e. algorithm analysis). Specifically, this thesis presents four major contributions corresponding to one peer-reviewed publication each, under the umbrella of ‘asymptotic reasoning in Isabelle/HOL’: The first of these introduces a proof automation tool that employs techniques from computer algebra to compute and prove limits and other asymptotic properties for a large class of real-valued functions (much like systems such as Maple or Mathematica). This tool has been instrumental in all my subsequent formalisation work, and no comparable instrumentation exists in other proof assistants. Second, a formal proof of a ‘cookbook method’ theorem due to Akra and Bazzi, which is a sweeping generalisation of the well-known Master Theorem of divide-and-conquer recurrences. In computer science, this theorem is a staple of the analysis of divide-and-conquer algorithms. The formalisation also provides tooling to facilitate the application of the theorem to specific algorithms. Third, a formalisation of the theory of linear recurrences and rational generating functions – in particular how to obtain closed-form solutions and asymptotic estimates of linear recurrences. These have applications in combinatorics and in the analysis of algorithms and data structures. In addition to the theorems, a verified executable solver for linear recurrences and a certifier for their asymptotics are also provided. Finally, in order to demonstrate the usability of the a, Diese Dissertation beschreibt meine Arbeit in der Formalisierung von Mathematik mit dem Beweisassistenten Isabelle/HOL, insbesondere von Mathematik im Zusammenhang mit asymptotischen Konzepten wie Grenzwerten und Funktionswachstum. Diese Arbeit beinhaltet sowohl die Formalisierung grundlegenden mathematischen Materials für die Isabelle/HOL-Standardbibliothek als auch die Etablierung neuer Werkzeuge zur Beweisautomatisierung. Beides wurde seitdem erfolgreich in vielen Anwendungen eingesetzt, sowohl Formalisierungen in der reinen Mathematik (wie Analysis und Zahlentheorie) als auch in der Informatik (z. B. Algorithmenanalyse). Konkret besteht diese Arbeit aus vier Teilen im Bereich „asymptotische Beweisführung in Isabelle/HOL“ mit jeweils einer zugehörigen Veröffentlichung: Der erste Teil ist ein Werkzeug zur Beweisautomatisierung, das Techniken aus der Computeralgebra verwendet, um Grenzwerte und andere asymptotische Eigenschaften für eine große Klasse von reellen Funktionen zu berechen und zu beweisen (ähnlich wie Systeme wie Maple oder Mathematica). Der zweite Teil beschreibt den formalen Beweis eines kochrezeptartigen Theorems von Akra und Bazzi, das eine Verallgemeinerung des bekannten Master-Theorems für „divide-and-conquer“-Rekurrenzen darstellt. Dieses Theorem ist ein grundlegender Bestandteil der Analyse von „divide-and-conquer“-Algorithmen in der Informatik. Die Formalisierung beinhaltet außerdem Werkzeuge, die die Anwendung des Theorems auf konkrete Algorithmen angenehmer gestalten. Der dritte Teil ist die Formalisierung der Theorie der linearen Rekurrenzen und rationalen Erzeugendenfunktionen – insbesondere wie geschlossene Lösungen und asymptotische Abschätzungen für sie gewonnen werden können. Diese finden Anwendungen in der Kombinatorik und der Analyse von Algorithmen und Datenstrukturen. Zusätzlich werden ein verifizierter ausführbarer Löser sowie eine Zertifizierer für asymptotische Abschätzungen entwickelt. Als letzter Punkt wird, um die Nutzbarkeit

Timed automata are a popular formalism for modeling real-time systems. Model checkers for timed automata can automatically prove the safety of such a model. This thesis addresses the question of the trustworthiness of these tools. In a first approach, a model checker for timed automata was constructed within the highly trustworthy theorem prover Isabelle/HOL. Next, unverified model checkers were modified to produce a proof for their result. An independent checker confirms that the proof is valid. By constructing the checker in Isabelle/HOL, the same level of trustworthiness is achieved., Timed Automata sind ein beliebter Formalismus, um Echtzeitsysteme zu modellieren. Model-Checker für Timed Automata können automatisch die Sicherheit eines solchen Modells beweisen. Diese Dissertation nimmt sich der Frage der Vertrauenswürdigkeit dieser Werkzeuge an. In einem ersten Ansatz wurde ein Model-Checker für Timed Automata innerhalb des höchst vertrauenswürdigen Theorembeweisers Isabelle/HOL konstruiert. Anschließend wurden unverifizierte Model-Checker modifiziert, um einen Beweis für ihr Ergebnis zu erzeugen. Ein unabhängiger Checker bestätigt, dass das Zertifikat korrekt ist. Durch Konstruktion des Checkers in Isabelle/HOL wird dasselbe Level von Vertrauenswürdigkeit erreicht.

In this thesis, I develop a verified compilation toolchain from executable specifications in Isabelle/HOL to CakeML abstract syntax trees. This improves over the state-of-the-art in Isabelle by providing a trustworthy procedure for code generation. The work consists of three major contributions: a certifying routine to eliminate type classes and instances, an algebra for higher-order Lambda-terms, and a compiler that works similarly to the existing code generator, but produces a CakeML abstract syntax tree together with a correctness theorem., Diese Dissertation entwickelt ein verifizierte Compiler-Toolkette von ausführbaren Spezifikationen in Isabelle/HOL zu abstrakten Syntaxbäumen in CakeML. Dies verbessert den Stand der Technik in Isabelle, indem es eine vertrauenswürdige Prozedur für Codegenerierung bereitstellt. Die Arbeit besteht aus drei Hauptbeiträgen: einer zertifizierende Routine zur Eliminierung von Typklassen und Instanzen, einer Algebra für höherstufige Lambda-Terme und einem Compiler, der ähnlich wie der existierende Codegenerator funktioniert, jedoch abstrakte CakeML-Syntax zusammen mit einem Korrektheitstheorem erzeugt.

Markov decision processes (MDPs) allow modeling decision-making in systems that exhibit both random and deterministic behavior. In our work, we extend an existing formalization of MDPs in the interactive theorem prover Isabelle/HOL. First, we introduce policies that formalize the strategy of the decision-maker. To assign a value to policies, we add reward functions to the MDP formalization. The problem arises of how to find an optimal policy, one that maximizes the rewards accumulated over time. We solve the problem by formalizing its Bellman equation and give conditions under which an optimal policy exists. Based on these developments, we verify the value iteration and policy iteration algorithms which compute (close to) optimal policies. This formalization may serve as a basis for future work on reinforcement learning algorithms, planning under uncertainty, and partially observable MDPs.

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.

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.

In this thesis, I develop a verified compilation toolchain from executable specifications in Isabelle/HOL to CakeML abstract syntax trees. This improves over the state-of-the-art in Isabelle by providing a trustworthy procedure for code generation. The work consists of three major contributions: a certifying routine to eliminate type classes and instances, an algebra for higher-order Lambda-terms, and a compiler that works similarly to the existing code generator, but produces a CakeML abstract syntax tree together with a correctness theorem., Diese Dissertation entwickelt ein verifizierte Compiler-Toolkette von ausführbaren Spezifikationen in Isabelle/HOL zu abstrakten Syntaxbäumen in CakeML. Dies verbessert den Stand der Technik in Isabelle, indem es eine vertrauenswürdige Prozedur für Codegenerierung bereitstellt. Die Arbeit besteht aus drei Hauptbeiträgen: einer zertifizierende Routine zur Eliminierung von Typklassen und Instanzen, einer Algebra für höherstufige Lambda-Terme und einem Compiler, der ähnlich wie der existierende Codegenerator funktioniert, jedoch abstrakte CakeML-Syntax zusammen mit einem Korrektheitstheorem erzeugt.

This thesis studies the formalization of graphs in the Isabelle/HOL proof assistant. It describes a library for directed graphs and discusses its usage for undirected graphs and certificates of planarity. A new technique for structuring and presenting proof obligations provides a convenient language for program verification. Building on these results, programs checking such planarity certificates are verified., Diese Dissertation befasst sich mit der Darstellung von Graphen in dem Theorembeweiser Isabelle/HOL. Sie beschreibt eine Formalisierung gerichteter Graphen und diskutiert die Anwendung auf ungerichtete Graphen und Planaritätszertifikate. Eine neue Technik zur Strukturierung und Präsentation von Beweisen bietet eine geeignete Sprache zur Programmverifikation, die dann auf Programme zur Überprüfung von Planaritätszertifikaten angewendet wird.

This thesis aims to promote types as a powerful tool for abstraction in the interactive theorem prover Isabelle/HOL. The first contribution is having solved an open question under which criteria types can be defined consistently in Isabelle/HOL. The second contribution is development of Transfer and Lifting, tools providing automation for building libraries of abstract types (subtypes and quotients). They are based on notions of Reynolds's relational parametricity and partial quotients., Diese Dissertation zielt darauf ab, Typen als ein mächtiges Werkzeug für die Abstraktion in dem interaktiven Theorembeweiser Isabelle/HOL zu fördern. Der erste Beitrag ist die Lösung der offenen Frage, unter welchen Kriterien die Typen in Isabelle/HOL konsistent definiert werden können. Der zweite Beitrag ist die Entwicklung von Transfer und Lifting, Werkzeuge für den Aufbau von Bibliotheken abstrakter Typen (Subtypen oder Quotienten). Sie basieren auf den Begriffen von Reynolds relationaler Parametrizität und partiellen Quotienten.

We study decision procedures for the equivalence of regular languages represented as regular expressions or logical formulas. Traditional algorithms in this context dispose of this symbolic representation by translating it into finite automata, which then are minimized and checked for structural equality. We develop concise algorithms that avoid this explicit translation by working with the symbolic structures directly. Our procedures are specified and proved correct in the proof assistant Isabelle., Wir beschäftigen uns mit Entscheidungsprozeduren für die Äquivalenz regulärer Sprachen, die durch reguläre Ausdrücke oder logische Formeln dargestellt sind. Traditionelle Algorithmen hierfür entledigen sich dieser symbolischen Darstellung, indem sie sie in endliche Automaten übersetzen, welche anschließend minimiert und auf strukturelle Gleichheit überprüft werden. Wir entwickeln kompakte funktionale Algorithmen, die diese explizite Übersetzung vermeiden und stattdessen mit der symbolischen Darstellung arbeiten. Unsere Entscheidungsprozeduren sind in dem Theorembeweiser Isabelle spezifiziert und ihre Korrektheit ist formal verifiziert.

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.

The goal of this work is the verification of probabilistic systems in the interactive theorem prover Isabelle/HOL. This requires the formalization of probability theory. We construct probability spaces with infinitely many independent random variables and the stochastic process of a Markov chain. We use these probability spaces to verify the correctness of probabilistic model checking and to verify properties of the ZeroConf protocol and the Crowds protocol., Ziel dieser Arbeit ist die Verifikation probabilistischer Systeme in dem interaktiven Theorembeweiser Isabelle/HOL. Dies setzt die Formalisierung von Wahrscheinlichkeitstheorie voraus. Wir konstruieren W-Räume mit unendlich vielen, unabhängigen Zufallsvariablen und den zu einer Markov-Kette gehörenden stochastischen Prozess. Wir verwenden diese W-Räume um die Korrektheit von probabilistischem Model Checking und Eigenschaften des ZeroConf-Protokolls und des Crowds-Protokoll zu verifizieren.

This thesis presents a counterexample generator for the interactive theorem prover Isabelle/HOL that uncovers faulty specifications and invalid conjectures using testing methods. Its contributions are two testing strategies: exhaustive testing with concrete values; and symbolic testing, evaluating conjectures with a narrowing strategy. We present techniques to deal with conditional conjectures, including an approach to synthesize test data generators derived from the premise's definition., Diese Dissertation beschreibt einen Gegenbeispielgenerator für den interaktiven Theorembeweiser Isabelle/HOL, der fehlerhafte Spezifikationen und ungültige Hypothesen durch Testmethoden aufdeckt. Ein Beitrag dieser Arbeit sind zwei neue Teststrategien: erschöpfendes Testen und symbolisches Testen mit einer Narrowing-Strategie. Die Arbeit beschreibt Techniken um mit bedingten Hypothesen umzugehen und die Synthese von Testdatengeneratoren, die aus der Definition der Bedingung erzeugt werden.

This thesis describes work on two components of the interactive theorem prover Isabelle/HOL. The primary contribution is the development of Nitpick, a counterexample generator that builds on a first-order relational model finder. The second main contribution is the further development of the Sledgehammer proof tool. This tool heuristically selects facts relevant to the conjecture to prove and delegates the problem to first-order resolution provers and SMT solvers., Diese Dissertation beschreibt die Arbeit an zwei Komponenten des interaktiven Theorembeweisers Isabelle/HOL. Der erste Beitrag ist die Entwicklung von Nitpick, einem Gegenbeispielgenerator, der auf einem erststufigen relationalen Modellfinder aufbaut. Der zweite Beitrag ist die Weiterentwicklung des Beweistools Sledgehammer. Dieses Tool wählt relevante Fakten aus und delegiert das Problem an erststufige Resolutionsbeweiser und SMT-Löser.

This thesis presents the first formalization of the Owicki-Gries method and its compositional version, the rely-guarantee method, in a theorem prover. These methods are widely used for correctness proofs of parallel imperative programs with shared variables. We define syntax, semantics and proof rules in Isabelle/HOL, which is the instantiation of higher-order logic in the theorem prover Isabelle. The proof rules also provide for programs parameterized in the number of parallel components. Their correctness w.r.t. the semantics is proven mechanically and the completeness proofs for both methods are extended to the new case of parameterized programs. For the automatic generation of verification conditions we define a tactic based on the proof rules. Using this tactic we verify several non-trivial examples for parameterized and non-parameterized programs., In dieser Arbeit wird die Owicki-Gries Methode, und ihre kompositionelle Version, die Rely-Guarantee Methode, zur Verifikation paralleler imperativer Programme mit gemeinsamen Variablen zum ersten Mal in einem Theorembeweiser formalisiert. Syntax, Semantik und Beweisregeln werden in höherstufiger Logik definiert und die Korrektheit des Beweissystems bezüglich der Semantik wird bewiesen. Zahlreiche Beispiele, darunter parametrisierte parallele Programme, werden mit Hilfe einer Taktik für die systematische Generierung der Verifikations-Bedingungen verifiziert. Außerdem wird die Vollständigkeit der formalisierten Systeme für den Fall parametrisierter paralleler Programme bewiesen.

Model checkers like SPIN provide a way to gain certainty about the behavior of programs and protocols. To guarantee that the model checker itself is correct, the CAVA project developed a verified and executable LTL model checker using Isabelle/HOL. This thesis reports on various building blocks of CAVA by presenting the first formalized and executable Promela semantics, a framework for verifying depth-first search based algorithms, and an automata library. As a part thereof, this thesis will detail the development rationale and history of those building blocks., Modelchecker, wie z.B. SPIN, sind eine Möglichkeit, Gewissheit über das Verhalten von Programmen und Protokollen zu erlangen. Um nun sicherzustellen, dass der Modelchecker selber korrekt ist, wurde im Projekt CAVA ein verifizierter und ausführbarer Modelchecker mit Hilfe von Isabelle/HOL entwickelt. In dieser Dissertation stellen wir verschiedene Bausteine von CAVA vor: Die erste formalisierte und ausführbare Semantik von Promela, ein Framework um auf Tiefensuche basierende Algorithmen zu verifizieren, sowie eine Automatenbibliothek. Ein Augenmerk liegt dabei auf der Geschichte und den Hintergründen der jeweiligen Implementierung.

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.

The aim of this thesis is to provide an infrastructure for general recursive function definitions in a proof assistant based on higher-order logic (HOL) that has no native support for recursion or pattern matching. In the first part we develop a tool that automates recursive function definitions and provides appropriate proof rules for them. Compared to previous work, our package supports the definition of partial functions, modeling the domain of the function by an inductive domain predicate. An automatically-generated partial induction rule makes partial correctness proofs independent from termination proofs. This modularity considerably facilitates termination arguments for nested recursions. The second part addresses the problem of automatically solving the termination proof obligations that arise from function definitions. Methods from the literature can be applied, but require significant adaptation to the specific needs of our setting: They must produce full formal proofs and work relative to a rich interactive theory. Our approach encompasses a rule-based selection of measure functions, a simple control-flow analysis inspired by the dependency-pairs approach, and a modified version of the size-change principle based on certificates. A formalization of the full size-change principle is also provided. In the third part we discuss how pattern matching, which occurs frequently in functional programming, can be supported in HOL function definitions. We present a very general form of pattern matching, where arbitrary expressions can serve as patterns. We show how such patterns can be encoded using a custom matching combinator and how their consistency can be expressed in proof obligations. We also study the problem of transforming ML-style sequential pattern matching into minimal sets of independent equations, such that they are consistent in HOL. We relate the problem to the minimization problem for propositional DNF formulas and show that it is $\Sigma_2^P$-comp, Ziel dieser Arbeit ist die Entwicklung einer Infrastruktur für rekursive Funktionsdefinitionen in einem interaktiven Theorembeweiser, in dem Rekursion und Pattern-Matching nicht von Haus aus unterstützt werden. Wir arbeiten im Kontext höherstufiger Logik (higher-order logic, HOL). Im ersten Teil entwickeln wir ein Werkzeug, welches Funktionsdefinitionen automatisiert und geeignete Beweisregeln dafür bereitstellt. Im Gegensatz zu existierenden Ansätzen unterstützt unser Verfahren auch partielle Funktionen, die mit Hilfe eines induktiven Domainprädikats modelliert werden. Eine automatisch generierte Induktionsregel erlaubt partielle Korrektheitsbeweise unabhängig von der Terminierung der Funktion. Diese modulare Struktur erleichtert insbesondere die Behandlung von geschachtelter Rekursion. Der zweite Teil behandelt automatische Terminierungsbeweise, um die aus Funktionsdefinitionen entstehenden Beweisverpflichtungen automatisch zu lösen. Dabei verwenden wir Methoden aus der Literatur, die allerdings an die spezifischen Anforderungen unseres Szenarios angepasst werden müssen. Unser Ansatz beinhaltet eine regelbasierte Auswahl von Maßfunktionen, eine einfache Kontrollflussanalyse ähnlich der Dependency-Pairs-Methode, und eine Variante des Size-Change-Kriteriums mit Zertifikaten. Eine Formalisierung des vollen Size-Change-Kriteriums wird ebenfalls entwickelt. Im dritten Teil untersuchen wir, wie das in der funktionalen Programmierung gebräuchliche Pattern-Matching in HOL unterstützt werden kann. Wir entwickeln eine sehr allgemeine Form von Pattern-Matching in der Logik, welches beliebige Terme als Patterns erlaubt und mit Hilfe eines speziellen Kombinators in der Logik ausgedrückt werden kann. Die Konsistenz der Spezifikation wird durch spezielle Beweisverpflichtungen sichergestellt. Außerdem untersuchen wir das Problem, Spezifikationen mit sequenziellem Pattern-Matching in reine Gleichungsspezifikationen mit möglichst wenigen Glei­chungen umzuwandeln. Wir ziehen eine Pa

This thesis is the second major contribution to the Flyspeck project which has as its goal the complete machine-verified formalization of the proof of the Kepler conjecture that Thomas Hales has given in 1998. We specify, generate and bound what Hales loosely calls the basic linear programs. We do this within the interactive proof assistant Isabelle. There are two major aspects of this work: Logical reasoning and trusted computing. Of course trusted computing can be considered as a special case of logical reasoning but requirements regarding the speed of computing demand a special treatment. Our solution to this problem is the HOL Computing Library. A substantial part of this work is dedicated to the design and implementation of this library. We then apply the library to show that 92.5% of all tame graphs give raise to basic linear programs which are inconsistent., Diese Arbeit ist der zweite größere Beitrag zum Flyspeck-Projekt, dessen Ziel die vollständige maschinelle Verifikation des Beweises der Keplerschen Vermutung ist, den Thomas Hales 1998 gegeben hat. Wir spezifizieren, generieren, und berechnen Schranken für die von Hales sogenannten elementaren linearen Programme, und zwar innerhalb des interaktiven Beweisassistenten Isabelle. Zwei Aspekte sind dabei prägend: Logisches Schließen und verlässliches Rechnen. Natürlich kann verlässliches Rechnen als Spezialfall von logischem Schließen angesehen werden aber Anforderungen an die Rechengeschwindigkeit verlangen nach einer gesonderten Lösung. Als solche stellen wir ein Programmpaket für verlässliches Rechnen vor. Ein beträchtlicher Teil unserer Arbeit ist dem Design und der Implementierung dieses Programmpakets gewidmet. Mit seiner Hilfe beweisen wir, dass 92,5% aller zahmen Graphen elementare lineare Programme induzieren, die inconsistent sind.

This thesis presents several extensions to the generic theorem prover Isabelle, a logical framework based on higher order logic. The central contribution of this thesis is the extension of Isabelle with a calculus of primitive proof terms, in which proofs are represented using lambda-terms in the spirit of the Curry-Howard isomorphism. Primitive proof terms allow for an independent verification of proofs constructed in Isabelle by a small and reliable proof checker, and are an important prerequisite for the application of proof transformation and analysis techniques, as well as the exchange of proofs with other systems. In particular, the proof term calculus is used to study the relationship between proofs and programs. For this purpose, we first develop a generic mechanism for the extraction of provably correct programs from constructive proofs, then instantiate it for the particular object logic Isabelle/HOL, and finally apply it to several case studies, ranging from simple textbook examples to complex applications from the field of combinatorics or the theory of lambda-calculus. Moreover, we introduce an alternative approach for obtaining programs from specifications by directly interpreting inductive definitions as logic programs., Diese Arbeit präsentiert mehrere Erweiterungen des generischen Theorembeweisers Isabelle. Der zentrale Beitrag der Arbeit ist die Erweiterung von Isabelle um einen Kalkül für primitive Beweisterme, in dem Beweise als Lambda-Terme repräsentiert werden. Primitive Beweisterme erlauben eine unabhängige Verifikation von in Isabelle konstruierten Beweisen durch einen kleinen und vertrauenswürdigen Beweisprüfer und bilden eine wichtige Voraussetzung für den Austausch von Beweisen mit anderen Systemen. Der Beweistermkalkül wird insbesondere dazu verwendet, um die Beziehung zwischen Beweisen und Programmen zu studieren. Hierzu wird ein Mechanismus zur Extraktion von beweisbar korrekten Programmen aus konstruktiven Beweisen entwickelt und auf verschiedene Fallstudien angewandt. Darüberhinaus stellen wir einen alternativen Ansatz zur Gewinnung von Programmen aus Spezifikationen vor, der induktive Definitionen direkt als Logikprogramme interpretiert.

The purpose of this thesis is to create a verification environment for sequential imperative programs. First a general language model is proposed, which is independent of a concrete programming language but expressive enough to cover all common language features: mutually recursive procedures, abrupt termination and exceptions, runtime faults, local and global variables, pointers and heap, expressions with side effects, pointers to procedures, partial application and closures, dynamic method invocation and also unbounded nondeterminism. For this language a Hoare logic for both partial and total correctness is developed and on top of it a verification condition generator is implemented. The Hoare logic is designed to allow the integration of program analysis or software model checking into the verification. To demonstrate the continuity to a real programming language a subset of C is embedded into the verification environment. The whole work is developed in the theorem prover Isabelle. Therefore the correctness is machine-checked and in addition the rich infrastructure of the general purpose theorem prover Isabelle can be employed for the verification of imperative programs., Ziel der Dissertation ist es, eine Verifikationsumgebung für sequentielle imperative Programme zu schaffen. Zunächst wird unabhängig von einer konkreten Programmiersprache ein allgemeines Sprachmodell entwickelt, das ausdrucksstark genug ist um alle gängigen Programmiersprachkonzepte abzudecken: Gegenseitig rekursive Prozeduren, abrupte Terminierung und Ausnahmebehandlung, Laufzeitfehler, lokale und globale Variablen, Zeiger und Halde, Ausdrücke mit Seiteneffekten, Zeiger auf Prozeduren, partielle Applikation, dynamischer Methoden Aufruf und unbeschränkter Indeterminismus. Für dieses Sprachmodell wird eine Hoare Logik sowohl für partielle alsauch für totale Korrektheit entwickelt. Darauf aufbauend wird ein Verifikations-Bedingungs-Generator implementiert. Die Hoare Logik erlaubt die Integration von statischer Programmanalyse und Software Model Checkern in die Verifikation. Desweiteren wird eine Teilsprache von C in die Verifikationsumgebung eingebettet, um die Durchgängigkeit zu einer realen Programmiersprache zu demonstrieren. Die gesamte Entwicklung wurde im Theorembeweiser Isabelle durchgeführt. Dadurch wird zum einen die Korrektheit maschinell sichergestellt und zum anderen steht nun für die Verifikation von Programmen die reichhaltige Infrastruktur einer vollwertigen und universellen Beweisumgebung zur Verfügung.

The rise of computational social choice indicates that a computer-science perspective can contribute to our understanding of collective decision making. In this thesis, we show how substantial insights can be achieved via computer-aided methods that are based on powerful solving techniques, such as SAT and SMT (satisfiability modulo theories). Our contribution is twofold: first and foremost, we provide such methods for the domain of social choice theory, and, second, use these methods to obtain a set of novel results that are of independent interest., Der Aufstieg des Forschungsgebiets "Computational Social Choice" deutet an, dass eine informatische Perspektive einen wesentlichen Beitrag zum Verständnis kollektiver Entscheidungsfindung leisten kann. In dieser Dissertation zeigen wir auf, wie wesentliche Erkenntnisse mithilfe computerunterstützter Methoden, die wiederum auf mächtigen Lösungsverfahren wie SAT und SMT ("Satisfiability Modulo Theories") basieren, generiert werden können. Unser Beitrag umfasst sowohl die Entwicklung solcher Methoden im Bereich der Sozialwahltheorie als auch die Anwendung dieser Methoden zur Erzeugung vielfältiger Ergebnisse, welche von unabhängigem Interesse sind.

The goal of this work is the verification of probabilistic systems in the interactive theorem prover Isabelle/HOL. This requires the formalization of probability theory. We construct probability spaces with infinitely many independent random variables and the stochastic process of a Markov chain. We use these probability spaces to verify the correctness of probabilistic model checking and to verify properties of the ZeroConf protocol and the Crowds protocol., Ziel dieser Arbeit ist die Verifikation probabilistischer Systeme in dem interaktiven Theorembeweiser Isabelle/HOL. Dies setzt die Formalisierung von Wahrscheinlichkeitstheorie voraus. Wir konstruieren W-Räume mit unendlich vielen, unabhängigen Zufallsvariablen und den zu einer Markov-Kette gehörenden stochastischen Prozess. Wir verwenden diese W-Räume um die Korrektheit von probabilistischem Model Checking und Eigenschaften des ZeroConf-Protokolls und des Crowds-Protokoll zu verifizieren.

This thesis presents a counterexample generator for the interactive theorem prover Isabelle/HOL that uncovers faulty specifications and invalid conjectures using testing methods. Its contributions are two testing strategies: exhaustive testing with concrete values; and symbolic testing, evaluating conjectures with a narrowing strategy. We present techniques to deal with conditional conjectures, including an approach to synthesize test data generators derived from the premise's definition., Diese Dissertation beschreibt einen Gegenbeispielgenerator für den interaktiven Theorembeweiser Isabelle/HOL, der fehlerhafte Spezifikationen und ungültige Hypothesen durch Testmethoden aufdeckt. Ein Beitrag dieser Arbeit sind zwei neue Teststrategien: erschöpfendes Testen und symbolisches Testen mit einer Narrowing-Strategie. Die Arbeit beschreibt Techniken um mit bedingten Hypothesen umzugehen und die Synthese von Testdatengeneratoren, die aus der Definition der Bedingung erzeugt werden.

This thesis presents two extensions to the theorem prover Isabelle/HOL, a logical framework based on higher-order logic. The main contribution is a model generator for higher-order logic that proceeds by translating the input formula to propositional logic, so that a standard SAT solver can be employed for the actual model search. The translation is proved correct. The model generator has been integrated with the Isabelle system, extended to support some of the definitional mechanisms provided by Isabelle/HOL, and applied to various case studies. Moreover, SAT solvers have been integrated with Isabelle in a proof-producing fashion: propositional tautologies can be proved by a SAT solver, and the resolution proof found by the solver is verified by Isabelle. An adequate representation of the problem allows to verify proofs with millions of resolution steps., Diese Arbeit präsentiert zwei Erweiterungen des Theorembeweisers Isabelle/HOL, einem auf Logik höherer Stufe basierenden System. Der Hauptbeitrag ist ein Modellgenerator für höherstufige Logik, der seine Eingabeformel in Aussagenlogik übersetzt, so dass ein herkömmlicher SAT-Solver für die eigentliche Modellsuche verwendet werden kann. Die Korrektheit der Übersetzung wird gezeigt. Der Modellgenerator ist in das Isabelle-System integriert worden, unterstützt verschiedene definitorische Mechanismen, wie sie in Isabelle/HOL zur Verfügung stehen, und ist auf mehrere Fallstudien angewandt worden. Darüber hinaus sind SAT-Solver beweisgenerierend mit Isabelle integriert worden: Aussagenlogische Tautologien können von einem SAT-Solver bewiesen werden, und der von dem Solver gefundene Resolutionsbeweis wird von Isabelle verifiziert. Eine günstige Repräsentation des Problems erlaubt die Verifikation von Beweisen mit mehreren Millionen Resolutionsschritten.

Code generation denotes the translation of an abstract formal specification into a corresponding executable program. The aim of this thesis is to present a code generator framework for the interactive proof assistant Isabelle/HOL, an implementation of higher-order logic. It comes with two substantial novelties: a general but lightweight concept for datatype abstraction and support for Isabelle type classes in the manner of Haskell type classes. Code can be generated for functional programming languages supporting pattern matching, concrete instances for SML, OCaml and Haskell are presented., Codegenerierung bezeichnet die automatische Überführung einer abstrakten formalen Spezifikation in ein korrespondierendes ausführbares Programm. Ziel dieser Arbeit ist die Darstellung eines Codegenerator-Frameworks für den interaktiven Theorembeweiser Isabelle/HOL, einer Implementierung höherstufiger Logik. Gegenüber existierenden Ansätzen weist das Framework zwei substantielle Neuerungen auf: ein sehr allgemeines, aber leichtgewichtiges Konzept für Datentypabstraktion und die Unterstützung von Isabelle-Typklassen im Sinne von Haskell-Typklassen. Konzeptionell möglich ist Generierung von Code für funktionale Sprachen mit Pattern Matching; konkrete Instantiierungen des Frameworks liegen vor für die Zielsprachen SML, OCaml und Haskell.

This work introduces a new model for optimizing transformations between attributed trees, targeted at the declarative specification of document formatters. The new model is based on rules incorporating constraints on the syntactic structure as well as semantic properties of source and target trees. A practical specification language based on the new model is developed. The applicability of the new approach is demonstrated by several examples., In dieser Arbeit wird ein neues Modell für optimierende Transformationen zwischen attributierten Bäumen eingeführt, das auf die deklarative Spezifikation von Dokumentformatierern abzielt. Das neue Modell basiert auf Regeln, die Konsistenzbedingungen bezüglich der syntaktischen Struktur sowie semantischer Eigenschaften von Quell- und Zielbäumen beinhalten. Es wird eine Spezifikationssprache basierend auf dem neuen Modell für den praktischen Einsatz entwickelt.

In an LCF-like theorem prover, any proof must be produced from a small set of inference rules. The development of automated proof methods in such systems is extremely important. In this thesis we study the following question: How should we integrate a proof procedure in an LCF-like theorem prover, both in general and in the special case of arithmetics? We investigate three integration paradigms and present several proof procedures. These include universal and weak existential problems over rings, universal polynomial problems over the reals, quantifier elimination for parametric linear problems over ordered fields, Presburger arithmetic, mixed real-integer linear arithmetic, algebraically and real closed fields. Our work has been carried out in the Isabelle framework., In einem LCF-ähnlichen Theorembeweiser, stammt jeder Beweis aus einer minimalen Menge von Inferenzregeln ab. Somit sind Verfahren zur Generierung solcher Beweise von enormer Wichtigkeit. Das Ziel dieser Abhandlung ist folgende Frage zu studieren: Wie soll, allgemein und im Spezialfall der Arithmetik, ein LCF-ähnlicher Theorembeweiser um eine Entscheidungsprozedur erweitert werden? Wir betrachten drei verschiedene Ansätze für eine solche Integration und präsentieren mehrere Beweisverfahren im Detail. Die wichtigsten präsentierten Verfahren sind: a) Entscheidungsprozeduren für universelle und schwach existentielle Probleme in Ringen, b) Univerelle Probleme reeller Polynome, c) Quantoren-elimination für parametrische lineare Formeln über geordnete Körper, Presburger Arithmetik, die gemischte lineare Theorie der reelen und ganzen Zahlen, Algebraisch- und Reel-abgeschlossene Körper. Alle unsere Arbeiten basieren auf dem Isabelle Theorembeweiser.

The purpose of this thesis is to create a coupling of the formal specification framework FOCUS in the generic theorem prover Isabelle/HOL, a logical framework based on Higher-Order Logic. The main focus of this work is on specification and verification of embedded real-time systems. The key contributions of the thesis are (1) Deep embedding of that part of the framework FOCUS, which is appropriate for the specification of real-time systems, into Isabelle/HOL. „FOCUS on Isabelle“ enables to validate and verify system specifications in a methodological way. (2) Syntax extensions for FOCUS for the argumentation over time intervals: a special kind of tables, timed state transition diagrams, and a number of new operators. The deep embedding into Isabelle/HOL includes all these extensions. (3) Schemata for automatic correctness proofs in Isabelle/HOL of the syntactic interfaces for specified system components., Das Ziel dieser Arbeit ist die Realisierung einer Kopplung des formalen Spezifikationssystems FOCUS mit dem generischen Theorembeweiser Isabelle/HOL zur rechnergestützte Verifikation von eingebetteten Echtzeitssystemen. Die zentralen Beiträge der Arbeit sind: (1) Tiefe Einbettung der Teile von FOCUS in Isabelle/HOL, die für die Spezifikation der Echtzeitsysteme angebracht sind. „FOCUS on Isabelle“, das Ergebnis der Kopplung, erlaubt Systemspezifikationen zu validieren und zu verifizieren. (2) FOCUS -Syntaxerweiterungen für die Argumentation über den Zeitintervallen: spezielle Tabellen, gezeitete Zustandsübergangsdiagramme und einige neue Operatoren. Die tiefe Einbettung in Isabelle/HOL umfasst alle diese Erweiterungen. (3) Schemata für automatische Korrektheitsbeweise in Isabelle/HOL von syntaktischen Schnittstellen der spezifizierten Systemkomponenten.

This thesis deals with machine-checking a large sublanguage of sequential Java, covering nearly all features, in particular the object-oriented ones. It shows that embedding such a language in a theorem prover and deducing practically important properties is meanwhile possible and explains in detail how this can be achieved. We formalize the abstract syntax, and the static semantics including the type system and well-formedness conditions, as well as an operational (evaluation) semantics of the language. Based on these definitions, we can express soundness of the type system, an important design goal claimed to be reached by the designers of Java, and prove that type safety holds indeed. Moreover, we give an axiomatic semantics of partial correctness for both statements and (side-effecting) expressions. We prove the soundness of this semantics relative to the operational semantics, and even prove completeness. We further give a small but instructive application example. A direct outcome of this work is the confirmation that the design and specification of Java (or at least the subset considered) is reasonable, yet some omissions in the language specification and possibilities for generalizing the design can be pointed out. The second main contribution is a sound and complete Hoare logic, where the soundness proof for our Hoare logic gives new insights into the role of type safety. To our knowledge, this logic is the first one for an object-oriented language that has been proved complete. By-products of this work are a new general technique for handling side-effecting expressions and their results, the discovery of the strongest possible rule of consequence, and a new rule for flexible handling of mutual recursion. All definitions and proofs have been done fully formally with the interactive theorem prover Isabelle/HOL, representing one of its major applications. This approach guarantees not only rigorous definitions, but also gives maximal confidence in the results, Diese Dissertation behandelt die maschinelle Analyse des (fast vollständigen) sequentiellen Teils der objektorientierten Programmiersprache Java. Wir zeigen, dass die Einbettung einer solchen Sprache in einen Theorembeweiser, in diesem Fall Isabelle/HOL, und der Beweis wichtiger metatheoretischer Eigenschaften inzwischen gut möglich ist. Dazu beschreiben wir detailliert die Formalisierung mit Abstrakter Syntax, Typsystem und der Operationellen Semantik sowie ein Anwendungsbeispiel, geben einen Beweis der Typsicherheit, entwickeln eine Axiomatische Semantik und beweisen deren Korrektheit und Vollständigkeit.

In an LCF-like theorem prover, any proof must be produced from a small set of inference rules. The development of automated proof methods in such systems is extremely important. In this thesis we study the following question: How should we integrate a proof procedure in an LCF-like theorem prover, both in general and in the special case of arithmetics? We investigate three integration paradigms and present several proof procedures. These include universal and weak existential problems over rings, universal polynomial problems over the reals, quantifier elimination for parametric linear problems over ordered fields, Presburger arithmetic, mixed real-integer linear arithmetic, algebraically and real closed fields. Our work has been carried out in the Isabelle framework., In einem LCF-ähnlichen Theorembeweiser, stammt jeder Beweis aus einer minimalen Menge von Inferenzregeln ab. Somit sind Verfahren zur Generierung solcher Beweise von enormer Wichtigkeit. Das Ziel dieser Abhandlung ist folgende Frage zu studieren: Wie soll, allgemein und im Spezialfall der Arithmetik, ein LCF-ähnlicher Theorembeweiser um eine Entscheidungsprozedur erweitert werden? Wir betrachten drei verschiedene Ansätze für eine solche Integration und präsentieren mehrere Beweisverfahren im Detail. Die wichtigsten präsentierten Verfahren sind: a) Entscheidungsprozeduren für universelle und schwach existentielle Probleme in Ringen, b) Univerelle Probleme reeller Polynome, c) Quantoren-elimination für parametrische lineare Formeln über geordnete Körper, Presburger Arithmetik, die gemischte lineare Theorie der reelen und ganzen Zahlen, Algebraisch- und Reel-abgeschlossene Körper. Alle unsere Arbeiten basieren auf dem Isabelle Theorembeweiser.

The purpose of this thesis is to create a coupling of the formal specification framework FOCUS in the generic theorem prover Isabelle/HOL, a logical framework based on Higher-Order Logic. The main focus of this work is on specification and verification of embedded real-time systems. The key contributions of the thesis are (1) Deep embedding of that part of the framework FOCUS, which is appropriate for the specification of real-time systems, into Isabelle/HOL. „FOCUS on Isabelle“ enables to validate and verify system specifications in a methodological way. (2) Syntax extensions for FOCUS for the argumentation over time intervals: a special kind of tables, timed state transition diagrams, and a number of new operators. The deep embedding into Isabelle/HOL includes all these extensions. (3) Schemata for automatic correctness proofs in Isabelle/HOL of the syntactic interfaces for specified system components., Das Ziel dieser Arbeit ist die Realisierung einer Kopplung des formalen Spezifikationssystems FOCUS mit dem generischen Theorembeweiser Isabelle/HOL zur rechnergestützte Verifikation von eingebetteten Echtzeitssystemen. Die zentralen Beiträge der Arbeit sind: (1) Tiefe Einbettung der Teile von FOCUS in Isabelle/HOL, die für die Spezifikation der Echtzeitsysteme angebracht sind. „FOCUS on Isabelle“, das Ergebnis der Kopplung, erlaubt Systemspezifikationen zu validieren und zu verifizieren. (2) FOCUS -Syntaxerweiterungen für die Argumentation über den Zeitintervallen: spezielle Tabellen, gezeitete Zustandsübergangsdiagramme und einige neue Operatoren. Die tiefe Einbettung in Isabelle/HOL umfasst alle diese Erweiterungen. (3) Schemata für automatische Korrektheitsbeweise in Isabelle/HOL von syntaktischen Schnittstellen der spezifizierten Systemkomponenten.

Proof Carrying Code (PCC) is a technique to exclude safety errors in low level code. Instead of runtime tests, it statically checks a proof of safety (a certificate) attached to the code. To guarantee that PCC only accepts safe code, we formalise and verify it in Isabelle/HOL, an interactive theorem prover for higher order logic. In an abstract framework we identify key components and their interfaces, specify requirements and prove theorems stating that accepted code is safe and under what conditions safe code can be certified. Our main contribution is a generic verification condition generator (VCG), which inspects code and emits proof obligations. By adjusting parameters, we instantiate this VCG to a Java-like bytecode language with objects, methods and exceptions. Bytecode with annotations in a first order assertion logic can be certified not to cause arithmetic overflow. To annotate code we integrate bytecode analysers for intervals and types. Finally, Isabelle's facilities for code generation, proof production and proof checking enable us to turn our formalisation into a runnable prototype., Proof Carrying Code (PCC) ist eine Technik zum Ausschluss von Sicherheitsfehlern in Maschinencode. Statt Laufzeittests durchzuführen, wird statisch ein Beweis (Zertifikat) geprüft. Um zu garantieren, dass ein solches System nur sicheren Code akzeptiert, formalisieren und verifizieren wir PCC in Isabelle/HOL, einem Beweissystem für höherstufige Logik. Wir beweisen, dass zertifizierter Code sicher ist, und unter welchen Voraussetzungen sich sicherer Code zertifizieren lässt. Der Hauptbeitrag ist ein generischer Verifikationsbedingungsgenerator (VCG), den wir für eine Teilsprache von Java-Bytecode instanziieren. Dieser VCG inspiziert Bytecode, der mit Formeln einer eigens geschaffenen Zusicherungssprache annotiert ist, und liefert Beweisverpflichtungen, die arithmetischen Überlauf und falsche Annotationen ausschließen. Annotationen können wir manuell oder mittels angebundener Analysatoren für Typen und Intervalle einfügen. Zur Gewinnung und Überprüfung der Zertifikate setzen wir wiederum Isabelle/HOL ein.

In 1998, Thomas Hales published a proof of the Kepler Conjecture, which states that the {m cubic close packing} is the densest possible packing of equally-sized spheres. The proof is by exhaustion on a set of 3050 plane graphs satisfying certain properties, called {m tame plane graphs}. The enumeration of this set has been generated by a computer program, hence the completeness of this enumeration is essential for the proof. In this thesis, we formalize a theory of plane graphs defined as an inductive set in the theorem prover Isabelle/HOL: a plane graph is constructed starting with one face and repeatedly adding new faces. Based on this theory, we formalize one part of the proof of the Kepler Conjecture, the completeness of the enumeration of tame plane graphs., Im Jahre 1998 veröffentlichte der Mathematiker Thomas Hales einen Beweis der auf Kepler zurückgehenden Vermutung, daß die kubisch dichte Kugelpackung (englisch {m cubic close packing}) die dichteste Kugelpackung ist. Der Beweis beruht auf einer umfangreichen, durch ein Programm generierten Fallunterscheidung über ca. 3050 Fälle. Dabei wird jeder Fall durch einen ebenen Graphen mit bestimmten Eigenschaften, einem sogenannten {m zahmen Graphen} repräsentiert. Wesentlich für den Beweis ist die Vollständigkeit dieser Aufzählung. In dieser Arbeit geht es um eine Formalisierung einer Theorie ebener Graphen in dem Theorembeweiser Isabelle/HOL, basierend auf einer Definition als induktive Menge: Eine Konstruktion eines ebenen Graphen beginnt mit einer einzigen Fäche, an die sukzessive neue Flächen angelegt werden. Darauf aufbauend wird ein Teil des Beweises der Kepler Vermutung formalisiert, die Vollständigkeit der Aufzählung der zahmen Graphen.

The basic motivation of this work is to make formal theory developments with machine-checked proofs accessible to a broader audience. Our particular approach is centered around the Isar formal proof language that is intended to support adequate composition of proof documents that are suitable for human consumption. Such primary proofs written in Isar may be both checked by the machine and read by human-beings; final presentation merely involves trivial pretty printing of the sources. Sound logical foundations of Isar are achieved by interpretation within the generic Natural Deduction framework of Isabelle, reducing all high-level reasoning steps to primitive inferences. The resulting Isabelle/Isar system is generic with respect to object-logics and proof tools, just as pure Isabelle itself. The full Isar language emerges from a small core by means of several derived elements, which may be combined freely with existing ones. This results in a very rich space of expressions of formal reasoning, supporting many viable proof techniques. The general paradigms of Natural Deduction and Calculational Reasoning are both covered particularly well. Concrete examples from logic, mathematics, and computer-science demonstrate that the Isar concepts are indeed sufficiently versatile to cover a broad range of applications., [Abstract nur auf Englisch verfügbar.] The basic motivation of this work is to make formal theory developments with machine-checked proofs accessible to a broader audience. Our particular approach is centered around the Isar formal proof language that is intended to support adequate composition of proof documents that are suitable for human consumption. Such primary proofs written in Isar may be both checked by the machine and read by human-beings; final presentation merely involves trivial pretty printing of the sources. Sound logical foundations of Isar are achieved by interpretation within the generic Natural Deduction framework of Isabelle, reducing all high-level reasoning steps to primitive inferences. The resulting Isabelle/Isar system is generic with respect to object-logics and proof tools, just as pure Isabelle itself. The full Isar language emerges from a small core by means of several derived elements, which may be combined freely with existing ones. This results in a very rich space of expressions of formal reasoning, supporting many viable proof techniques. The general paradigms of Natural Deduction and Calculational Reasoning are both covered particularly well. Concrete examples from logic, mathematics, and computer-science demonstrate that the Isar concepts are indeed sufficiently versatile to cover a broad range of applications.

The bytecode verifier is an important part of Java's security architecture. This thesis presents a fully formal, executable, and machine checked specification of a representative subset of the Java Virtual Machine and its bytecode verifier together with a proof that the bytecode verifier is safe. The specification consists of an abstract framework for bytecode verification which is instantiated step by step with increasingly expressive type systems covering all of the interesting and complex properties of Java bytecode verification: classes, objects, inheritance, virtual methods, exception handling, constructors, object initialization, bytecode subroutines, and arrays. The instantiation yields two executable verified bytecode verifiers: the iterative data flow algorithm of the standard Java platform and also a lightweight bytecode verifier for resource-constrained devices such as smart cards. All specifications and proofs have been carried out in the interactive theorem prover Isabelle/HOL. Large parts of the proofs are written in the human-readable proof language Isabelle/Isar making it possible to understand and reproduce the reasoning independently of the theorem prover. All formal proofs in this thesis are machine checked and generated directly from Isabelle sources., Der Bytecode Verifier ist ein essentieller Bestandteil der Sicherheitsarchiktektur der Programmierplattform Java. Die Dissertation präsentiert eine formale, ausführbare Spezifikation des Bytecode Verifiers sowie den Beweis, dass dieser korrekt ist. Die Formalisierung im Theorembeweiser Isabelle besteht aus einem abstrakten Framework für Bytecode-Verifikation, das mit zunehmend ausdrucksstarken Typsystemen instantiiert wird. Diese decken sämtliche interessanten Eigenschaften der Java-Plattform ab: Klassen, Objekte, virtuelle Methoden, Vererbung, Ausnahmebehandlung, Konstruktoren, Objekt-Initialisierung, Subroutinen und Felder. Die Formalisierung liefert zwei ausführbare verifizierte Bytecode Verifier: den iterativen Standard-Algorithmus sowie einen Lightweight Bytecode Verifier für Geräte mit eingeschränkten Ressourcen.

The purpose of this thesis is to create a verification environment for sequential imperative programs. First a general language model is proposed, which is independent of a concrete programming language but expressive enough to cover all common language features: mutually recursive procedures, abrupt termination and exceptions, runtime faults, local and global variables, pointers and heap, expressions with side effects, pointers to procedures, partial application and closures, dynamic method invocation and also unbounded nondeterminism. For this language a Hoare logic for both partial and total correctness is developed and on top of it a verification condition generator is implemented. The Hoare logic is designed to allow the integration of program analysis or software model checking into the verification. To demonstrate the continuity to a real programming language a subset of C is embedded into the verification environment. The whole work is developed in the theorem prover Isabelle. Therefore the correctness is machine-checked and in addition the rich infrastructure of the general purpose theorem prover Isabelle can be employed for the verification of imperative programs., Ziel der Dissertation ist es, eine Verifikationsumgebung für sequentielle imperative Programme zu schaffen. Zunächst wird unabhängig von einer konkreten Programmiersprache ein allgemeines Sprachmodell entwickelt, das ausdrucksstark genug ist um alle gängigen Programmiersprachkonzepte abzudecken: Gegenseitig rekursive Prozeduren, abrupte Terminierung und Ausnahmebehandlung, Laufzeitfehler, lokale und globale Variablen, Zeiger und Halde, Ausdrücke mit Seiteneffekten, Zeiger auf Prozeduren, partielle Applikation, dynamischer Methoden Aufruf und unbeschränkter Indeterminismus. Für dieses Sprachmodell wird eine Hoare Logik sowohl für partielle alsauch für totale Korrektheit entwickelt. Darauf aufbauend wird ein Verifikations-Bedingungs-Generator implementiert. Die Hoare Logik erlaubt die Integration von statischer Programmanalyse und Software Model Checkern in die Verifikation. Desweiteren wird eine Teilsprache von C in die Verifikationsumgebung eingebettet, um die Durchgängigkeit zu einer realen Programmiersprache zu demonstrieren. Die gesamte Entwicklung wurde im Theorembeweiser Isabelle durchgeführt. Dadurch wird zum einen die Korrektheit maschinell sichergestellt und zum anderen steht nun für die Verifikation von Programmen die reichhaltige Infrastruktur einer vollwertigen und universellen Beweisumgebung zur Verfügung.

This thesis presents several extensions to the generic theorem prover Isabelle, a logical framework based on higher order logic. The central contribution of this thesis is the extension of Isabelle with a calculus of primitive proof terms, in which proofs are represented using lambda-terms in the spirit of the Curry-Howard isomorphism. Primitive proof terms allow for an independent verification of proofs constructed in Isabelle by a small and reliable proof checker, and are an important prerequisite for the application of proof transformation and analysis techniques, as well as the exchange of proofs with other systems. In particular, the proof term calculus is used to study the relationship between proofs and programs. For this purpose, we first develop a generic mechanism for the extraction of provably correct programs from constructive proofs, then instantiate it for the particular object logic Isabelle/HOL, and finally apply it to several case studies, ranging from simple textbook examples to complex applications from the field of combinatorics or the theory of lambda-calculus. Moreover, we introduce an alternative approach for obtaining programs from specifications by directly interpreting inductive definitions as logic programs., Diese Arbeit präsentiert mehrere Erweiterungen des generischen Theorembeweisers Isabelle. Der zentrale Beitrag der Arbeit ist die Erweiterung von Isabelle um einen Kalkül für primitive Beweisterme, in dem Beweise als Lambda-Terme repräsentiert werden. Primitive Beweisterme erlauben eine unabhängige Verifikation von in Isabelle konstruierten Beweisen durch einen kleinen und vertrauenswürdigen Beweisprüfer und bilden eine wichtige Voraussetzung für den Austausch von Beweisen mit anderen Systemen. Der Beweistermkalkül wird insbesondere dazu verwendet, um die Beziehung zwischen Beweisen und Programmen zu studieren. Hierzu wird ein Mechanismus zur Extraktion von beweisbar korrekten Programmen aus konstruktiven Beweisen entwickelt und auf verschiedene Fallstudien angewandt. Darüberhinaus stellen wir einen alternativen Ansatz zur Gewinnung von Programmen aus Spezifikationen vor, der induktive Definitionen direkt als Logikprogramme interpretiert.

The basic motivation of this work is to make formal theory developments with machine-checked proofs accessible to a broader audience. Our particular approach is centered around the Isar formal proof language that is intended to support adequate composition of proof documents that are suitable for human consumption. Such primary proofs written in Isar may be both checked by the machine and read by human-beings; final presentation merely involves trivial pretty printing of the sources. Sound logical foundations of Isar are achieved by interpretation within the generic Natural Deduction framework of Isabelle, reducing all high-level reasoning steps to primitive inferences. The resulting Isabelle/Isar system is generic with respect to object-logics and proof tools, just as pure Isabelle itself. The full Isar language emerges from a small core by means of several derived elements, which may be combined freely with existing ones. This results in a very rich space of expressions of formal reasoning, supporting many viable proof techniques. The general paradigms of Natural Deduction and Calculational Reasoning are both covered particularly well. Concrete examples from logic, mathematics, and computer-science demonstrate that the Isar concepts are indeed sufficiently versatile to cover a broad range of applications., [Abstract nur auf Englisch verfügbar.] The basic motivation of this work is to make formal theory developments with machine-checked proofs accessible to a broader audience. Our particular approach is centered around the Isar formal proof language that is intended to support adequate composition of proof documents that are suitable for human consumption. Such primary proofs written in Isar may be both checked by the machine and read by human-beings; final presentation merely involves trivial pretty printing of the sources. Sound logical foundations of Isar are achieved by interpretation within the generic Natural Deduction framework of Isabelle, reducing all high-level reasoning steps to primitive inferences. The resulting Isabelle/Isar system is generic with respect to object-logics and proof tools, just as pure Isabelle itself. The full Isar language emerges from a small core by means of several derived elements, which may be combined freely with existing ones. This results in a very rich space of expressions of formal reasoning, supporting many viable proof techniques. The general paradigms of Natural Deduction and Calculational Reasoning are both covered particularly well. Concrete examples from logic, mathematics, and computer-science demonstrate that the Isar concepts are indeed sufficiently versatile to cover a broad range of applications.