The Foundations of Algorithmic Verification group at the Max Planck Institute for Software Systems in Saarbruecken, Germany, headed by Joel Ouaknine, has several open postdoc positions in the area of algorithmic verification and analysis of dynamical systems. The overall goal of the project is to develop techniques to solve fundamental computational problems arising in the verification of discrete and continuous linear dynamical systems, including Markov chains, linear recurrence sequences, linear while loops, linear differential equations, hybrid systems, and infinite-state systems. You will develop algorithms to solve reachability, termination, and synthesis problems for these models by combining a range of computational techniques, including results from number theory (particularly lower bounds in Diophantine approximation). In cases where algorithms cannot be obtained, you will seek reductions from known "hard" problems. The project aims to build on, and significantly develop, recent progress at MPI-SWS and Oxford in solving long-standing open problems in this area. You should have a PhD (or be close to completion) in a relevant area of computer science, mathematics, or a related discipline, together with a documented track record of the ability to conduct and complete research projects in automated verification, automata theory, dynamical systems, or algorithmic algebra and number theory. To apply, please send CV and short statement of purpose to Joel Ouaknine <joel@mpi-sws.org>, with Annika Meiser <ameiser@mpi-sws.org> in cc, before the closing date of ***22 April 2019***. Informal inquiries of course very welcome. -- *Joël Ouaknine* Max Planck Institute for Software Systems, Saarland Informatics Campus, Germany Department of Computer Science, Oxford University, UK http://mpi-sws.org/~joel/ <http://people.mpi-sws.org/~joel/>