Are you passionate about deep learning, generative AI, agents? We are seeking a postdoctoral researcher to join the research group led by Ivan Titov (http://ivan-titov.org/), part of the natural language processing group of the Institute for Logic, Language and Computation (ILLC).

This position is supported by a prestigious Swedish Research Council grant focused on automatic synthesis of programs for spatial Multi-Agent Systems. The research centers on developing foundational theories and practical techniques for the formal verification of autonomous systems, including controller synthesis, planning, and model checking.

Competitive candidates are expected to have a background, and experience of working with one (or more) of the following:

• Formal methods (e.g., concurrency, automata, or temporal/spatial logics, etc) or discrete control (e.g., planning, supervisory control, or controller synthesis, etc.)
• Verification tools such as Model Checkers, Synthesis Engines, etc.
• Prior experience in combining reinforcement learning with reactive synthesis and/or control is a plus.

This PhD project is at the intersection of verification and machine learning and covers both the analysis of software and cyber-physical systems and the analysis of learning-enabled systems.

Computer-aided verification of AI systems connects the fields of formal methods, machine learning and software engineering. It combines classical symbolic verification methods as well as novel machine learning methods for safe and trustworthy AI. Potential research topics include, but are not limited to, developing methods to guarantee that cyber-physical systems with deep learning components are safe and ensuring that software and hardware components are correct. 

The Institute of Computer Science of the Czech Academy of Sciences in Prague is advertising a postdoctoral position, to join the Czech Science Foundation project Model theory, structural combinatorics, and algorithms, led by Samuel Braunfeld. Expertise in model theory alone (or combinatorics alone) is fine.

The anticipated start date is in the fall of 2026 (negotiable), and would provide funding until the end of 2028. Applications received by January 16, 2026 will be guaranteed full consideration, but later applications will continue to be considered until the position is filled. 

The Mathematical Insights into Algorithms for Optimization (MIAO) group are looking for a researcher with strong mathematical background combined with excellent algorithmic thinking and programming skills to further expand our world-leading work on certifying algorithms. There is some flexibility as to what kind of research members of the group pursue, though, and all candidates are welcome, both those who want to go deep into either theory or practice and those who are inspired by the challenge of bridging the gap between the two.

The employment duration is for two years. The starting date is negotiable, but should ideally be in August-September 2026 or earlier. 

The Mathematical Insights into Algorithms for Optimization (MIAO) group are looking for a mathematically gifted PhD student with excellent programming skills to continue our ground-breaking work on certifying algorithms, funded by the Wallenberg AI, Autonomous Systems and Software Program (WASP). There is some flexibility as to what kind of research PhD students in the group pursue, though, and all candidates are welcome, both those who want to go deep into either theory or practice and those who are inspired by the challenge of bridging the gap between the two.

This PhD position is a four-year full-time employed positions; it might include 20% teaching, in which case it will be prolonged for one more year. The starting date is negotiable, but should ideally be in August-September 2026 or earlier. 

Applications are invited for a PhD studentship at UCL with project title 'A Foundational Theory of Information Based on Inference'. The joint supervisors are Tim Button and David Pym. UK and international candidates can be considered.

This project at University College London aims to study a version of incorrectness logic with novel logical foundations and analysis techniques that can formally prove the presence of bugs in randomised software. The PhD will provide training in programming principles, logic, and formal verification. Candidates should have a Bachelor's degree in computer science or mathematics. Ideal candidates should have a Master's degree with a solid technical background and interest in programming languages and logical methods in computer science.

The KU Leuven Faculty of Engineering Technology has a vacancy at Campus De Nayer for a full-time professor in Intelligent Software that combines machine learning and knowledge-based inference.
The candidate will be embedded in the DTAI section of the KU Leuven Department of Computer Science and EAVISE - KULeuven.

The Department of Computer Science at the University of Bath is seeking to appoint two lecturers in cybersecurity, who will join the Mathematical Foundations of Computation group.

The applicant should have a research interests around fundamental aspects of cybersecurity, including but not limited to post-quantum cryptography, formal methods and verification, complexity, logical systems and type theory.

The IMPRS for Language Sciences invites applications for PhD fellowships that are funded by the Max Planck Society for the Advancement of Science. 

The position relevant for the ILLC audience is within the Language and Computation in Neural Systems (LaCNS) Project. An ideal candidate should holds (or soon will hold) a Research Master’s degree (or equivalent) in linguistics, psycholinguistics, cognitive science, cognitive neuroscience, computer science, or a related field.