Christoph Haase, Samin Ishtiaq, Joel Ouaknine, and Matthew Parkinson
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 graphbased 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-theart tools by orders of magnitude.
In Computer Aided Verification (CAV)