Keyword:Isabelle/HOL

Papers
Efficient Formalization of Simplification Orders René Thiemann and Akihisa Yamada EasyChair Preprint no. 8639
Competitive Proving for Fun Maximilian Paul Louis Haslbeck and Simon Wimmer In:Selected Student Contributions and Workshop Papers of LuxLogAI 2018
Extending a Verified Simplex Algorithm René Thiemann In:LPAR-22 Workshop and Short Paper Proceedings
A Verified Efficient Implementation of the LLL Basis Reduction Algorithm Ralph Bottesch, Max W. Haslbeck and René Thiemann In:LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann EasyChair Preprint no. 396
Reasoning about Translation Lookaside Buffers Hira Syeda and Gerwin Klein In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
My Life with an Automatic Theorem Prover Jasmin Christian Blanchette In:Proceedings of the 1st and 2nd Vampire Workshops
Formal Replay of Translation Validation for Highly Optimised C Thomas Sewell In:VPT 2014. Second International Workshop on Verification and Program Transformation
A Framework for Verified Depth-First Algorithms René Neumann In:ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation
Redirecting Proofs by Contradiction Jasmin Christian Blanchette In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs Steffen Juilf Smolka and Jasmin Christian Blanchette In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Towards High-Assurance Multiprocessor Virtualisation Michael von Tessin In:VERIFY-2010. 6th International Verification Workshop