Quis Custodiet

Chair for Logic and Verification

Overview

Quis Custodiet Ipsos Custodes – who will guard the guards? Who guarantees the correctness of program analyses? The aim of this joint project (with the Programming Paradigms group of Gregor Snelting at KIT) was twofold: the formal verification of program analyses with the help of Isabelle (at KIT) and the development of new tools for the automatic proof of theorems and automatic search for counterexamples to conjectures in Isabelle (at TUM).

The main results of the project at TUM were:

Funding: DFG Project 47694595, 2007–2013

Key Publications

  1. Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson. LEO-II and Satallax on the Sledgehammer test bench. In: J. Appl. Log. 11(1): 91-102 (2013)

  2. Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson. Extending Sledgehammer with SMT Solvers. In: J. Autom. Reason. 51(1): 109-128 (2013)

  3. Jasmin Christian Blanchette. Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. In: Softw. Qual. J. 21(1): 101-126 (2013)

  4. Steffen Juilf Smolka, Jasmin Christian Blanchette. Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. In: Proof eXchange for Theorem Proving (PxTP@CADE): 117-132 (2013)

  5. Jasmin Christian Blanchette, Andrei Paskevich. TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. In: International Conference on Automated Deduction (CADE): 414-420 (2013)

  6. Jasmin Christian Blanchette, Andrei Popescu. Mechanizing the Metatheory of Sledgehammer. In: Frontiers of Combining Systems (FroCoS): 245-260 (2013)

  7. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban: MaSh: Machine Learning for Sledgehammer. In: Interactive Theorem Proving (ITP): 35-50 (2013)

  8. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone. Encoding Monomorphic and Polymorphic Types. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS): 493-507 (2013)

  9. Jasmin Christian Blanchette. Automatic proofs and refutations for higher-order logic. Doctoral thesis, Technical University Munich (2012)

  10. Lukas Bulwahn. Counterexample generation for higher-order logic using functional and logic programming. Doctoral thesis, Technical University Munich (2012)

  11. Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach. More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. In: Interactive Theorem Proving (ITP): 345-360 (2012)

  12. Lukas Bulwahn. The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof. In: Certified Programs and Proofs (CPP): 92-108 (2012)

  13. Lukas Bulwahn. Smart Testing of Functional Programs in Isabelle. In: Logic for Programming, Artificial Intelligence and Reasoning (LPAR): 153-167 (2012)

  14. Jasmin Christian Blanchette, Alexander Krauss. Monotonicity Inference for Higher-Order Formulas. In: J. Autom. Reason. 47(4): 369-398 (2011)

  15. Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson. Extending Sledgehammer with SMT Solvers. In: International Conference on Automated Deduction (CADE): 116-130 (2011)

  16. Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow. Automatic Proof and Disproof in Isabelle/HOL. In: Frontiers of Combining Systems (FroCoS): 12-27 (2011)

  17. Lukas Bulwahn. Smart test data generators via logic programming. In: International Conference on Logic Programming (ICLP): 139-150 (2011)

  18. Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar. Nitpicking C++ concurrency. In: Principles and Practice of Declarative Programming (PPDP): 113-124 (2011)

  19. Andreas Lochbihler, Lukas Bulwahn. Animating the Formalised Semantics of a Java-Like Language. In: Interactive Theorem Proving (ITP): 216-232 (2011)

  20. Jasmin Christian Blanchette, Alexander Krauss. Monotonicity Inference for Higher-Order Formulas. In: International Joint Conference on Automated Reasoning (IJCAR): 91-106 (2010)

  21. Jasmin Christian Blanchette, Tobias Nipkow. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In: Interactive Theorem Proving (ITP): 131-146 (2010)

  22. Lawrence C. Paulson, Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In: International Workshop on the Implementation of Logics (IWIL@LPAR): 1-11 (2010)

  23. Jasmin Christian Blanchette, Koen Claessen. Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models. In: Logic for Programming, Artificial Intelligence and Reasoning (LPAR): 127-141 (2010)