A pushdown system is a triple P=(P,Γ,Δ) where P and Γ are finite sets called the control locations and the stack alphabet, respectively. A configuration is a pair p,w, such that pP and wΓ, i.e., a control location with a sequence of stack elements. The finite set Δ is composed of rules. A rule has the form p,γp,w, where p,pP, γΓ, and wΓ.

[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.