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.
|Talk abstract (Pldi15.Abstract.mp4)||4.46MiB|
Tue 16 JunDisplayed time zone: Tijuana, Baja California change
14:00 - 15:40
|DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs|
Research PapersMedia Attached File Attached
|Exploring and Enforcing Security Guarantees via Program Dependence Graphs|
Andrew Johnson Harvard University, Lucas Waye Harvard University, Scott Moore Harvard University, Stephen Chong Harvard UniversityMedia Attached
|Making Numerical Program Analysis Fast|
Research PapersMedia Attached
|Tree Dependence Analysis|
Yusheng Weijiang Purdue University, Shruthi Balakrishna Purdue University, Jianqiao Liu Purdue University, Milind Kulkarni Purdue UniversityMedia Attached