2007 | OriginalPaper | Chapter
Program Analysis Using Weighted Pushdown Systems
Authors : Thomas Reps, Akash Lal, Nick Kidd
Published in: FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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
$\langle{p,S}\rangle$
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 that add 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.