Resourceful Reachability as HORN-LA
- Cite this paper as:
- Berdine J., Bjørner N., Ishtiaq S., Kriener J.E., Wintersteiger C.M. (2013) Resourceful Reachability as HORN-LA. In: McMillan K., Middeldorp A., Voronkov A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg
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.
Unable to display preview. Download preview PDF.