Research and Development Engineer in Formal Methods - 12 months contract

Who we are ? Télécom Paris, part of the IMT (Institut Mines-Télécom) and a founding member of the Institut Polytechnique de Paris, is one of France's top 6 general engineering schools. The mainspring of Télécom Paris is to train, imagine and undertake to design digital models, technologies and solutions for a society and economy that respect people and their environment. Modern distributed systems are increasingly complex, with multiple interconnected components, services, and autonomous agents interacting in dynamic environments. Ensuring their cybersecurity requires analysing both potential attacks and the strategies that defenders can adopt in response. Attackers may exploit sequences of vulnerabilities to compromise a system, while defenders may react through countermeasures such as access restrictions, system reconfigurations, or Moving Target Defense mechanisms. Traditional cybersecurity analysis techniques often focus on identifying vulnerabilities and possible attack paths, with limited support for reasoning about the strategic interactions between attackers and defenders. The VITAMIN-C (VerIficaTion of A MultI-ageNt system for Cybersecurity) project aims to address these challenges through formal verification. Building on VITAMIN, an existing modular model-checking platform for multi-agent systems, the project develops methods and tools for modelling and verifying cybersecurity properties in distributed and autonomous systems. Attackers and defenders are represented