Andrew Reynolds

A Decision Procedure for Separation Logic in SMT

2016 · arXiv (Cornell University)

This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic ($\seplog$) interpreted over heaplets with data elements ranging over a parametric multi-sorted (possibly infinite) domain. The algorithm uses a combination …