@inproceedings{berdine2013resourceful,
author = {Berdine, Josh and Bjørner, Nikolaj and Ishtiaq, Samin and Kriener, Jael E. and Wintersteiger, Christoph M.},
title = {Resourceful Reachability as HORN-LA},
booktitle = {International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
year = {2013},
month = {December},
abstract = {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.},
publisher = {Springer},
url = {http://approjects.co.za/?big=en-us/research/publication/resourceful-reachability-as-horn-la/},
edition = {International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
}