Reachability Modulo Theories

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.