Automated Mutual Explicit Induction Proof in Separation Logic

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo +1

We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, called mutual explicit inducti…