Proving Theorems of Higher-Order Logic with SMT Solvers
Sascha Böhme · mediaTUM – the media and publications repository of the Technical University Munich (Technical University Munich) · 2012
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.