Automata over infinite alphabets: Investigations in Fresh-Register Automata

While automata theory has traditionally been based on the model of an abstract machine operating on a finite alphabet of input symbols, this assumption can be unsatisfactory for a range applications where value domains cannot be reasonably bounded: from XML model-checking, to process modelling and the verification of name-generating code. This has recently lead to a surge of interest in automata over infinite alphabets, thus opening up a world of open problems and new results. The talk will look into these exciting developments with a specific focus on latest work driven by applications in modelling and verifying name-generating programs.

Short biography

Nikos Tzevelekos is a Senior Lecturer at the School of Electronic Engineering and Computer Science at Queen Mary University of London.

Previously, he was a postdoctoral researcher at the Department of Computer Science at the University of Oxford, where he also completed his PhD thesis. His focus is on semantics of programming languages. He devises mathematical models of programming languages, expressed using game semantics, and he examines applications of these models to program analysis for formally analysing and checking code.