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.     «

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 inge...     »

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.     «

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önn...     »