Foundations of Stack-Based Automata – LIFOUNDATIONS

Stack-based automata provide a mathematical framework for modeling the sequential behavior of computer programs.
They are essentially finite state automata that have access to an infinite memory that can be manipulated in a first-in/last-out fashion. Pushdown automata are probably the most prominent stack-based automata, allowing to model the behavior of recursive programs with boolean variables.



This project contributes to the foundational understanding of stack-based automata, a central model in software verification allowing to reason about sequentiality. It studies three central questions, namely the subclass problem (decide if a given program can be described by a simpler program of a
syntactical/semantical subclass), the complexity problem (decide if the computation realized by a given program can be performed using only a limited amount of resources) and and the equivalence problem (do two given programs behave equivalently?).

Although in the past twenty-five years several decidability results have been obtained, still many questions (sometimes very basic) remain open and are in some instances far from being understood.

The goal of this project is to improve our understanding of stack-based automata in terms of three central research directions: the subclass problem, the complexity problem, and the equivalence problem.