Template-Based Conjecturing for Automated Induction in Isabelle/HOL
- Venue: The 10th IPM International Conference on Fundamentals of Software Engineering (FSEN 2023)
- Location: Tehran, Iran
- Authors: Yutaka Nagashima, Zijin Xu, Ningli Wang, Daniel Sebastian Goc, and James Bang
- https://doi.org/10.1007/978-3-031-42441-0_9
Abstract
Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human engineers often have to provide auxiliary lemmas manually. We automate this laborious process with template-based conjecturing, a novel approach to generate auxiliary lemmas and use them to prove final goals. Our evaluation shows that our working prototype, TBC, achieved 50% point improvement of success rates for problems at intermediate difficulty level.
Project Dependency Graph
Mindmap
