Conditional weighted pushdown systems and applications

Pushdown systems are well understood as abstract models of programs with (recursive) procedures. Reps et al. recently extended pushdown systems into weighted pushdown systems, which serve as a generalized framework for solving certain kinds of meet-overall-path problems in program analysis. In this paper, we extend weighted pushdown systems to conditional weighted pushdown systems, by further specifying conditions under which a pushdown transition rule can be applied, and show that model checking problems on conditional weighted pushdown systems can be reduced to those on weighted pushdown systems. There are wider applications of conditional weighted pushdown systems when analyzing programs with objected-oriented features, for which weighted pushdown systems is not precise enough under a direct application. As an example, we lift a stacking-based pointsto analysis for Java designed in the framework of weighted pushdown systems to a more precise counterpart in the framework of conditio...

• Type: Conference
• Year: 2010
• Where: PEPM
• Authors: Xin Li, Mizuhito Ogawa
• Keywords: Conditional Weighted Pushdown, Keywords Weighted Pushdown, PEPM 2010, Software Engineering, Weighted Pushdown Systems