Resourceful Reachability as HORN-LA

  • Josh Berdine
  • Nikolaj Bjørner
  • Samin Ishtiaq
  • Jael E. Kriener
  • Christoph M. Wintersteiger
Conference paper

DOI: 10.1007/978-3-642-45221-5_10

Part of the Lecture Notes in Computer Science book series (LNCS, volume 8312)
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

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Josh Berdine
    • 1
  • Nikolaj Bjørner
    • 1
  • Samin Ishtiaq
    • 1
  • Jael E. Kriener
    • 1
  • Christoph M. Wintersteiger
    • 1
  1. 1.Microsoft ResearchUniversity of KentUK

Personalised recommendations