A pushdown system is a triple where and are finite sets called the control locations and the stack alphabet, respectively. A configuration is a pair , such that and , i.e., a control location with a sequence of stack elements. The finite set is composed of rules. A rule has the form , where , , and .
 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.