Analyzing pushdown systems with stack manipulation

Pushdown systems with transductions (TrPDSs) are an extension of pushdown systems (PDSs) by associating each transition rule with a transduction, which allows to inspect and modify the stack content at each step of a transition rule. In this work, we propose two novel saturation procedures to compute p r e ⁎ ( C ) and p o s t ⁎ ( C ) for finite TrPDSs. From these two saturation procedures, we present two algorithms to compute p r e ⁎ ( C ) and p o s t ⁎ ( C ) that are suitable for implementation. We also show that the algorithms for computing p r e ⁎ ( C ) and p o s t ⁎ ( C ) also work for weak finite TrPDSs, where closure is defined with respect to the underlying PDSs. These results are extended to left contextual TrPDSs, which is an extension of finite TrPDSs. Finally, we show how the presence of transductions enables the modeling of Boolean programs with call-by-reference parameter passing and low-level assembly programs that manipulate the program stack content via a stack pointer.

Authors

• Fu Song

Keywords

• Reachability analysis
• Pushdown systems
• Saturation procedure
• Boolean program
• Software verification