Reachability Analysis of Pushdown Systems with an Upper Stack

Adrien Pommellet, Marcio Diaz, Tayssir Touili

Pushdown systems (PDSs) are a natural model for sequential programs, but they can fail to accurately represent the way an assembly stack actually operates. Indeed, one may want to…