Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Corral: A Solver for Reachability Modulo Theories

Akash Lal, Shaz Qadeer, and Shuvendu Lahiri


Consider a sequential programming language with control flow constructs such as assignments, choice, loops, and procedure calls. We restrict the syntax of expressions in this language to one that can be efficiently decided by a satisfiability-modulo-theories solver. For such a language, we define the problem of deciding whether a program can reach a particular control location as the reachability-modulo-theories problem. This paper describes the architecture of Corral, a semi-algorithm for the reachability-modulo-theories problem. It further describes the novel algorithms that comprise the various components of Corral. Finally, the paper presents evaluation of Corral against other related tools. Corral consistently outperforms its competitors on most benchmarks.


Publication typeTechReport
> Publications > Corral: A Solver for Reachability Modulo Theories