Phd and internship subjects

Internship subjects

• A Toolbox for Handling Infinite Sets of Graphs

The goal of this internship is an implementation of a toolbox that handles sets of graphs described as regular grammars. Ideally, such a toolbox should support the boolean operations of union, intersection and complement and decide the problems of membership and inclusion, by building finite recognizer algebras from the syntactic description of sets, as regular grammars.

• Verifying Concurrent Systems with Automata over Infinite Alphabets

The goal of this internship is to study extensions of finite-state automata over infinite alphabets and apply them to the verification of concurrent and distributed systems with unbounded numbers of threads. The internship comprises theoretical as well as implementation work, and will explore orthogonal domains, such as logic, automata theory and concurrency.