LIFOUNDATIONS
About
The project LIFOUNDATIONS is funded by the French research agency
and studies the foundations of infinite-state systems that employ a last-in first-out (LIFO) behavior.
The central model we study are stack-based automata, which are finite-state automata
that can manipulate an infinite data structure in a LIFO fashion, as for instance pushdown
automata.
The study of these models has applications in software verification (reasoning
abstractions of computer programs that still allows to account for their call and return behavior)
such as in Moped,
in compiler testing but also
in the verification of security protocols.
Although many theoretical questions for stack-based automata have already been answered,
there are at least as many that are yet not really understood.
The LIFOUNDATIONS project studies three fundamental themes:
-
the subclass problem, i.e. to decide if a given stack-based automaton admits a simpler behavior
for some subclass of stack-based automata.
-
the complexity problem, to classify the computational complexity of the computing power
of a given stack-based automata.
-
the equivalence problem, to decide if two given stack-based automata behave equivalently.
For further questions, please contact Stefan Göller.
Project members
Scientific Documents