@inproceedings{lal2013reachability,
author = {Lal, Akash and Qadeer, Shaz},
title = {Reachability Modulo Theories},
booktitle = {7th International workshop on Reachability Problems (Invited Paper)},
year = {2013},
month = {September},
abstract = {Program verifiers that attempt to verify programs automatically pose the verification problem as the decision problem: "Does there exist a proof that establishes the absence of errors?" In this paper, we argue that program verification should instead be posed as the following decision problem: "Does there exist an execution that establishes the presence of an error?" We formalize the latter problem as Reachability Modulo Theories (RMT) using an imperative programming language parameterized by a multi-sorted first-order signature. We present complexity results, algorithms, and the Corral solver for the RMT problem. We present our experience using Corral on problems from a variety of application domains.},
url = {http://approjects.co.za/?big=en-us/research/publication/reachability-modulo-theories/},
edition = {7th International workshop on Reachability Problems (Invited Paper)},
}