SeLoger: A tool for graph-based reasoning in Separation Logic

This paper introduces the tool SeLoger, which is a reasoner for satisfiability and entailment in a fragment of Separation Logic with pointers and linked lists. SeLoger builds upon and extends graph-based algorithms that have recently been introduced in order to settle both decision problems in polynomial time. Running SeLoger on standard benchmarks shows that the tool outperforms current state-of-the-art tools by orders of magnitude.

Proceedings of CAV 13, LNCS 8044, 2013. 6 pages.

PDF © 2013 Springer-Verlag.