Template-Based Conjecturing for Automated Induction in Isabelle/HOL

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,