Keyword:interactive theorem proving

Publications
Mechanising Hall’s Theorem for Countable Graphs Fabián Fernando Serrano Suárez, Mauricio Ayala-Rincón and Thaynara Arielly de Lima EasyChair Preprint 10365
Verified Erasure Correction in Coq with MathComp and VST Joshua M. Cohen, Qinshi Wang and Andrew W. Appel EasyChair Preprint 8636
Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols Using the Squirrel Proof Assistant David Baelde, Stephanie Delaune, Adrien Koutsos and Solène Moreau EasyChair Preprint 8631
Generating Custom Set Theories with Non-Set Structured Objects Ciarán Dunne, Joe Wells and Fairouz Kamareddine EasyChair Preprint 5663
Automated Theorem Proving via Interacting with Proof Assistants by Dynamic Strategies Guangshuai Mo, Yan Xiong, Wenchao Huang and Lu Ma EasyChair Preprint 3334
Binary-compatible verification of filesystems with ACL2 Mihir Mehta and William R. Cook EasyChair Preprint 1235
Tactic Learning and Proving for the Coq Proof Assistant Lasse Blaauwbroek, Josef Urban and Herman Geuvers In:LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
A Mechanised Semantics for HOL with Ad-hoc Overloading Johannes Åman Pohjola and Arve Gengelbach In:LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Competitive Proving for Fun Maximilian Paul Louis Haslbeck and Simon Wimmer In:Selected Student Contributions and Workshop Papers of LuxLogAI 2018
Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions J Moore and Marijn Heule In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Formally Proving the Boolean Pythagorean Triples Conjecture Luís Cruz-Filipe and Peter Schneider-Kamp In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Compass-free Navigation of Mazes Phil Scott and Jacques Fleuriot In:SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
Tool Presentation: Isabelle/HOL for Reachability Analysis of Continuous Systems Fabian Immler In:ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems
Machine Learning of Coq Proof Guidance: First Experiments Cezary Kaliszyk, Lionel Mamane and Josef Urban In:SCSS 2014. 6th International Symposium on Symbolic Computation in Software Science
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora Cezary Kaliszyk and Josef Urban In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Escape to Mizar from ATPs Jesse Alama In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod Jasmin Christian Blanchette In:LPAR-17-short. short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning.
Towards High-Assurance Multiprocessor Virtualisation Michael von Tessin In:VERIFY-2010. 6th International Verification Workshop