Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Resourceful Reachability as HORN-LA

Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, and Christoph M. Wintersteiger


The program verification tool SLAyer uses abstractions during analysis and relies on a solver for reachability to refine spurious counterexamples. In this context, we extract a reachability benchmark suite and evaluate methods for encoding reachability properties with heaps using Horn clauses over linear arithmetic. The benchmarks are particularly challenging and we describe and evaluate pre-processing transformations that are shown to have significant effect.


Publication typeInproceedings
Published inInternational Conference on Logic for Programming, Artificial Intelligence and Reasoning
> Publications > Resourceful Reachability as HORN-LA