Automated mutual induction proof in separation logic

• Published in: Formal aspects of computing 2019-04, Vol.31 (2), p.207-230
• Main Authors: Ta, Quang-Trung, Le, Ton Chanh, Khoo, Siau-Cheng, Chin, Wei-Ngan
• Format: Article
• Language: English
• Subjects: Benchmarks; Computer Science; Logic; Math Applications in Computer Science; Mathematical models; Original Article; Separation; Theory of Computation
• ISSN: 0934-5043; 1433-299X
• DOI: 10.1007/s00165-018-0471-5

We present a deductive proof system to automatically prove separation logic entailments by mathematical induction. Our technique is called the mutual induction proof . It is an instance of the well-founded induction, a.k.a., Noetherian induction. More specifically, we propose a novel induction principle based on a well-founded relation of separation logic models. We implement this principle explicitly as inference rules so that it can be easily integrated into a deductive proof system. Our induction principle allows a goal entailment and other entailments derived during the proof search to be used as hypotheses to mutually prove each other. This feature increases the success chance of proving the goal entailment. We have implemented this mutual induction proof technique in a prototype prover and evaluated it on two entailment benchmarks collected from the literature as well as a synthetic benchmark. The experimental results are promising since our prover can prove most of the valid entailments in these benchmarks, and achieves a better performance than other state-of-the-art separation logic provers.