DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs

A hierarchical program is one with multiple procedures but no loops or recursion. This paper studies the problem of deciding reachability queries in hierarchical programs. This problem is fundamental to verification and most directly applicable to doing bounded reachability in programs, i.e., reachability under a bound on the number of loop iterations and recursive calls.

The usual method of deciding reachability in hierarchical programs is to first
inline all procedures and then do reachability on the resulting single-procedure program.
Such inlining unfolds the call graph of the program to a tree and may lead to an exponential
increase in the size of the program. We design and evaluate a method called DAG inlining that unfolds the call graph to a DAG instead of a tree by sharing the bodies of procedures at certain points during inlining. DAG inlining can produce much more compact representations than tree inlining. Empirically, we show that it leads to significant improvements in a state-of-the-art verifier.

A recorded talk of this work, presented at a workshop in ETH Zurich, can be found here:

http://www.srl.inf.ethz.ch/workshop2015.php