The importance of information technology in our daily lives is forcing us to rely on algorithms and computer systems for increasingly crucial aspects of our lives. Whether it is our private life threatened by increasingly virulent and sophisticated attacks against sites hosting our personal data, or decisions concerning us taken, in part, by algorithms (for example, ParcoursSup for post-back-orientation, or artificial intelligence intervening in the detection of tumours), or our physical integrity when travelling in vehicles that integrate more and more decision-making software.

The MTV (Models and Technologies for Verification) team has been developing techniques and tools for the safe operation of computer systems for many years. Notably the AltaRica language which is now used by several major players in the aeronautics industry for aircraft modelling and certification. The MTV team is also involved in the formal proof of the ParcoursSup post-baccalaureate orientation programme. More recently, a partnership has been established with the LaBRI "Progress" team around "trusted computing". This project explores on the one hand, the link between program proof and software testing, and on the other hand, the integration of program proof in software engineering practices. And on the other hand, cyber-security, with the objective of improving the robustness of systems by taking into account the complexity of current information systems, by aggregating the skills from various research themes: operating systems, networks, simulation, artificial intelligence, operating safety, etc.