Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic

Christoph Haase, Samin Ishtiaq, Joel Ouaknine, and Matthew Parkinson

Abstract

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.

Details

Publication typeProceedings
Published inComputer Aided Verification (CAV)
> Publications > SeLoger: A Tool for Graph-Based Reasoning in Separation Logic