Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Reachability Modulo Theories

Akash Lal and Shaz Qadeer

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.

Details

Publication typeInproceedings
Published in7th International workshop on Reachability Problems (Invited Paper)
> Publications > Reachability Modulo Theories