Dear colleagues,
I am thrilled to announce that our paper, “Template-Based Conjecturing for Automated Induction in Isabelle/HOL,” has been accepted for presentation at the 10th IPM International Conference on Fundamentals of Software Engineeringhttp://fsen.ir/2023/.
In this paper, we propose a novel approach to automated induction in Isabelle/HOL, using template-based conjecturing. Our method significantly reduces the proof search space and enables efficient reasoning about complex properties.
Here’s a brief summary of our findings:
Proof by induction is an essential tool in formal verification, but automating it remains a formidable challenge in computer science. To tackle this issue, we developed a method that automates the process of generating auxiliary lemmas to solve inductive problems. Our prototype, TBC, achieved a 40% increase in success rates for problems at the intermediate difficulty level, as we demonstrate in our evaluation.
The pre-print of this paper is available on arXiv.
The conference will take place from May 3 to May 5. We are looking forward to sharing our work and engaging with the research community.
I would like to take this opportunity to express my gratitude to my co-authors at Huawei Cambridge Research Centre for their valuable contributions and to the conference reviewers for their insightful feedback.
Thank you all for your support.
Best regards,
Yutaka
United Reasoning 