Option "Algorithmes et Méthodes Formelles"

L'option "Algorithmes et Methodes 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:

Stages et devenir des étudiants

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:

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 (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, 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.

Contenu des enseignements

La formation est constituée, d'une part, d'un enseignement d'introduction à la conception formelle de logiciels, qui comprend notamment une forte part d'application des connaissance au travers de projets avec TLA+ et Frama-C, et d'une initiation à la recherche (voir ci-dessous). Et d'autre part, de l'un des deux parcours suivants au choix:

Modèles & Algorithmes

  • Théorie des graphes avancée & algorithmique distribuée
  • Logique et langage
  • 2 parmi:
    • Vérification logicielle
    • Jeux, synthèse et contrôle
    • Complexité & algorithmique appliquée

Vérification logicielle

  • Vérification logicielle
  • Jeux, synthèse et contrôle
  • 1 parmi:
    • Théorie des graphes avancée & algorithmique distribuée
    • Systèmes de types & preuve
  • 1 parmi:
    • Logique & langages
    • Complexité & algorithmique appliquée

Initiation à la recherche

Les étudiants sont sensibilisés à la recherche lors des cours (bibliographie, etc.), et également au travers d'enseignements dédiés:

Renseignements complémentaires & partenariats

La formation est commune avec le master informatique de l'université de Bordeaux. Une description détaillée des enseignements est disponible dans le syllabus de l'ENSEIRB-MATMECA. Les transparents de présentation sont disponibles ici.

Contact: Frédéric Herbreteau (fh@enseirb-matmeca.fr)