Program Analysis Using Weighted Pushdown Systems

Abstract. Pushdown systems (PDSs) are an automata-theoretic formalism for specifying a class of infinite-state transition systems. Infiniteness comes from the fact that each configuration p, S in the state space consists of a (formal) “control location” p coupled with a stack S of unbounded size. PDSs can model program paths that have matching calls and returns, and automaton-based representations allow analysis algorithms to account for the infinite control state space of recursive programs. Weighted pushdown systems (WPDSs) are a generalization of PDSs a general “black-box” abstraction for program data (through weights). WPDSs also generalize other frameworks for interprocedural analysis, such as the Sharir-Pnueli functional approach. This paper surveys recent work in this area, and establishes a few new connections with existing work.

• Type: Conference
• Year: 2007
• Where: FSTTCS
• Authors: Thomas W. Reps, Akash Lal, Nicholas Kidd
• Keywords: FSTTCS 2007, Infinite-state Transition Systems, Pushdown Systems, State Space