A Decision Procedure for Well-Founded Reachability

In earlier work, we introduced the logic of well-founded reachability for reasoning about linked data structures. In this paper, we present a rewriting-based decision procedure for the ground (quantifier-free) logic. We also extend the logic with restricted set constraints to allow specifications involving unbounded collections of objects. We have implemented this decision procedure within a satisfiability modulo theories (SMT) framework. Our implementation substantially improves the automation and the time taken for verifying our benchmarks compared to our earlier approach based on an incomplete axiomatization of well-founded reachability.