Résumé | Multi-stack pushdown systems are natural models for capturing the control flow of multi-threaded programs. The intuition of exploring computations up to a bounded number of context switches has stimulated a series of interesting results in program verification, such as for example the possibility of sequentializing concurrent programs without maintaining the cross-product of the involved threads, and the study of the formal theory of decidable subclasses.
In this talk, we focus on the formal languages theory of the classes of MPS with the bounded-context switching, scope-bounded, phase-bounded, and stack-ordered restrictions. We also discuss some related results in verification. |