The project LIFOUNDATIONS is funded by the French research agency DigiCosme 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:
For further questions, please contact Stefan Göller.

Project members

Scientific Documents