A pushdown system is a triple $\mathcal{P}=\left(P,\mathrm{\Gamma },\mathrm{\Delta }\right)$ where $P$ and $\mathrm{\Gamma }$ are finite sets called the control locations and the stack alphabet, respectively. A configuration is a pair $\ll p,w\gg$, such that $p\in \mathcal{P}$ and $w\in {\mathrm{\Gamma }}^{\ast }$, i.e., a control location with a sequence of stack elements. The finite set $\mathrm{\Delta }$ is composed of rules. A rule has the form $\ll p,\gamma \gg \to \ll {p}^{\prime },w\gg$, where $p,{p}^{\prime }\in \mathcal{P}$, $\gamma \in \mathrm{\Gamma }$, and $w\in {\mathrm{\Gamma }}^{\ast }$.

[0] Späth, Johannes, Karim Ali, and Eric Bodden. “Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems.” Proceedings of the ACM on Programming Languages 3.POPL (2019): 48.