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 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.

HaaseCAV2013.pdf
PDF file

In  Computer Aided Verification (CAV)

Details

TypeProceedings
> Publications > SeLoger: A Tool for Graph-Based Reasoning in Separation Logic