Automated Lemma Synthesis in Symbolic-Heap Separation Logic

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

The symbolic-heap fragment of separation logic has been actively developed and advocated for verifying the memory-safety property of computer programs. At present, one of its bigge…