Tue 16 Jun 2015 14:00 - 14:25 at PLDI Main BLUE (Portland 254-255) - Analysis Chair(s): Yannis Smaragdakis

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.45MiB

Tue 16 Jun

14:00 - 15:40: Research Papers - Analysis at PLDI Main BLUE (Portland 254-255)
Chair(s): Yannis SmaragdakisUniversity of Athens
pldi2015-papers14:00 - 14:25
Akash LalMicrosoft Research India, Shaz QadeerMicrosoft Research
Media Attached File Attached
pldi2015-papers14:25 - 14:50
Andrew JohnsonHarvard University, Lucas WayeHarvard University, Scott MooreHarvard University, Stephen ChongHarvard University
Media Attached
pldi2015-papers14:50 - 15:15
Gagandeep SinghETH Zurich, Switzerland, Markus PüschelETH Zurich, Martin VechevETH Zurich
Media Attached
pldi2015-papers15:15 - 15:40
Yusheng WeijiangPurdue University, Shruthi BalakrishnaPurdue University, Jianqiao LiuPurdue University, Milind KulkarniPurdue University
Media Attached