Automated Reasoning About Recursive Programs

Purpose and goal

The purpose of this project was to explore applications for automating reasoning by induction, which is required for verification of recursive programs (e.g. functional languages like Haskell). In particular, to automate the discovery of additional lemmas or generalisations that otherwise often must be done by a human expert. We did indeed move the state-of-the-art in inductive theorem proving forwards by integrating theory exploration to enrich the background theory available to the prover.

Results and expected effects

The results from the project has been published in several articles and presented at international conferences. The project has also contributed to the development of the softwaresystems HipSpec and Hipster, both publicly available online (open source). We have also compiled a benchmark suite for evaluating and comparing inductive theorem provers. These are also available online for the benefit of other developers and researchers. The project has also led to new international collaborations and funding for subsequent research projects in the area.

Approach and implementation

When starting at Chalmers, I initialised a collaboration with researchers in the functional programming group. They had developed a tool for generating specifications for Haskell programs (QuickSpec) which we then came to integrate with an inductive prover in the system HipSpec. We showed that this system could automate many open inductive problems, following the theory exploration approach I had proposed and setting a new state-of-the-art for automated inductive theorem proving. This approach is now being implemented and developed also in other systems.