Abstract
I shall present several recent complexity results regarding standard decision problems (reachability, equivalence, bisimilarity) for register and pushdown register automata, developed in connection with applying automata over infinite alphabets in program verification. Some of the results rely on group theory to capture the inherent symmetries as well as techniques from computational group theory. This is joint work with Steven Ramsay and Nikos Tzevelekos that appeared in MFCS, LICS and ATVA.