3 citations · 7 across the 7 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2017
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…
cs.LO2016★ 1 cited
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…