Efficient path conditions in dependence graphs

Program slicing combined with constraint solving is a powerful tool for software analysis. Path conditions are generated for a slice or chop, which-when solved for the input variables-deliver compact "witnesses" for dependences or illegal influences between program points. We show how to make path conditions work for large programs. Aggressive engineering, based on interval analysis and BDDs, is shown to overcome the potential combinatoric explosion. Case studies and empirical data demonstrate the usefulness of path conditions for practical program analysis.