Option "Algorithmes et Méthodes Formelles"

L'option "Algorithmes et Méthodes Formelles (AMF)" forme des ingénieurs-chercheurs spécialistes en algorithmique, logique, modélisation et vérification formelle. Elle a pour objectifs de former de futurs ingénieurs aux dernières avancées académiques dans ces domaines, ainsi que de former les étudiants à la recherche. La formation est adossée aux équipes "Combinatoire et algorithmiques" et "Méthodes formelles" du LaBRI qui jouissent d'une forte reconnaissance nationale et internationale. Les débouchés de la formation concernent aussi bien l'entreprise que le monde académique, notamment la poursuite en doctorat, que ce soit en laboratoire de recherche académique ou en partenariat avec une entreprise. Les élèves-ingénieurs sont formés aux métiers de l'algorithmique (ingénieur algorithme, optimisation, performance) et de la vérification formelle (ingénieur méthodes formelles, sûreté de fonctionnement).

Compétences visées par la formation:

• Identifier la complexité d'un problème, proposer une solution efficace exacte si possible, ou approchée lorsque le problème est difficile.
• Modélisation, vérification et conception formelles d'algorithmes, de programmes et de systèmes.
• Réalisation d'une bibliographie, présentation de travaux de recherche, synthèse de documents scientifiques.

Quelques exemples de stages:

• Validation des logiciels embarqués critiques à l'aide de méthodes formelles (Easymile)
• Spécification et vérification de propriétés de haut niveau pour les programmes C (CEA Saclay)
• Vérification formelle de modèles dysfonctionnels (Thalès)
• Développer une implantation de l'algorithme PDR dans l'outil Systerel Smart Solver (Systerel)
• Algorithmes d'approximation pour le calcul de diamètre de grands graphes (LaBRI)
• Accessibilité dans les graphes planaires avec pannes (LaBRI)
• Application d'algorithmes de machine-learning à des problématiques industrielles (Delfox)
• Spécification et vérification formelle d'applications interactives cognitiques (IRIT/ONERA)
• L'exploitation de préférences dans l'accès aux données médiatisées par des ontologies (LaBRI)
• Hypergraph decompositions for #sat (Crystal)
• Preuve de propriétés sur des algorithmes à base d'IA (Thales)
• Propriétés formelles de confiance, de robustesse et d'équité de modèle d'IA dans caisar (CEA)

Les collaborations académiques et industrielles des chercheurs du LaBRI offrent de nombreuses opportunités de stages en entreprise comme en laboratoire de recherche, en France et à l'étranger.

L'employabilité des étudiants à la sortie de la formation est excellente. Certains étudiants poursuivent en doctorat (Laboratoires universitaires, CEA Saclay, Huawei, etc). D'autres préfèrent un emploi d'ingénieur, que ce soit au sein d'un projet de recherche académique ou dans une entreprise (Clearsy railway, SNCF, Systerel, Thalès, etc). Les connaissances et compétences développées dans la formation sont recherchées par secteurs d'activités: l'industrie des systèmes critiques (Thalès, Airbus, Alstom, EasyMile, etc.), le développement de logiciels et de services (Amazon S3, Microsoft, Oracle, etc.), les éditeurs de logiciels d'ingénierie système (Systerel, Clearsy, etc), et bien d'autres encore.