SeLoger: A Tool for Graph-Based Reasoning in Separation Logic - Haase, Christoph; Ishtiaq, Samin; Ouaknine, Joel; Parkinson, Matthew J. (Computer Aided Verification (CAV), 2013)
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.