About the Role:

Join us to push the state of the art in formal verification and reachability analysis for discrete-space systems. Your research will center on the applications of logical zonotopes in digital circuits and model checking of discrete-space systems, with the goal of building methodologies and tools that make verification scalable and reliable. Learn more about logical zonotopes: [paper link] | [talk link]. You will conduct original research on logical zonotope based methods for model checking and digital circuit verification. Also, you will design and implement prototypes (C++/Python/MATLAB) and contribute to open-source tooling where appropriate. You will support teaching at Technical University of Munich. Salary and benefits are in accordance with the German public sector scale, TV-L E13.

Your Qualification:

1. Strong mathematical background (e.g., linear algebra, optimization, formal methods, convex geometry).
2. Master's degree or PhD in Computer Science, Electrical Engineering, Control Systems, or a closely related field.
3. Experience in reachability analysis, formal verification/model checking, control theory, or related domains
4. Programming proficiency in C++, Python, MATLAB, or similar.

How to Apply:

Email Amr Alanwar (alanwar@tum.de) with the subject line Position in Logical Zonotopes and include:

1. CV (with publications and contact info for ≥2 references).
2. Academic transcripts

Applications are reviewed on a rolling basis; shortlisted candidates will be invited to interview.