Option "Algorithmes et Méthodes Formelles"
Présentation
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. 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).
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. La formation peut
être complétée par une poursuite en doctorat, que ce soit en
laboratoire de recherche académique, dans un organisme de recherche
(CEA, ONERA, etc) ou en partenariat avec une entreprise.
Compétences
Connaissances et compétences visées par la formation:
- Identifier la complexité d'un problème. Application à la résolution
efficace exacte (si possible), ou approchée de problèmes complexes
(optimisation, etc).
- Calcul distribué, calcul quantique, application à l'algorithmique
distribuée
- Modélisation, vérification et synthèse formelles. Application à la
conception formelle de programmes corrects.
- Réalisation d'une bibliographie, présentation de travaux de recherche,
synthèse de documents scientifiques.
Stages de fin d'études
La formation académique (voir ci-dessous) est complétée par un stage
de fin d'étude de 6 mois. Il peut se dérouler aussi bien en entreprise
qu'en laboratoire de recherche. Il peut aussi bien s'agir d'un stage
de recherche, incluant une démarche scientifique, que d'un stage
d'application des connaissances et compétences acquises lors de la
formation.
Quelques exemples de stages:
- Validation des logiciels embarqués critiques à l'aide de méthodes
formelles (Easymile)
- Contribution au développement et à la maintenance de Coluna, un framework open-source pour l'implémentation d'algorithmes d'optimisation (Atoptima)
- 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)
- 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)
- Développement d'algorithmes distribués pour la gestion d'équipements (Thélio)
- Hypergraph decompositions for #sat (Crystal)
Intégration professionnelle
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.
Programme d'enseignement
Semestre 9
La formation est constituée des unités d'enseignement suivantes dispensées
par le master informatique de l'Université de Bordeaux:
Obligatoire:
Au choix (21 ECTS):
Elle comprend également l'UE suivante dispensée par le département
informatique de l'ENSEIRB-MATMECA:
Semestre 10
Le semestre 10 est majoritairement consacré au stage de fin d'études.
Pour le diplôme de Master informatique, il comprend également deux UEs
qui ont lieu en janvier:
Aspects administratifs
- Les cours débutent début septembre
- Les enseignements peuvent avoir lieu en anglais (niveau B2 validé, de préférence)
- Inscription en master 2 informatique à l'Université de Bordeaux (double diplôme)
Renseignements complémentaires & partenariats
La formation est commune avec le
master informatique de l'université de Bordeaux. Une description détaillée
est disponible sur cette
page (uniquement semestres 9 et 10).
Contact: Frédéric Herbreteau (frederic.herbreteau@enseirb-matmeca.fr)
Date de dernière mise à jour: 11/5/2026
