Mention « Sciences du logiciel »

Présentation générale

Frédéric Boulanger
frederic.boulanger@centralesupelec.fr

Janvier 2026

Présentation

Frédéric Boulanger frederic.boulanger@centralesupelec.fr

Responsable de la mention « Sciences du logiciel »

Recherche

Laboratoire Méthodes Formelles (LMF)

Responsable de la thématique :
« Modélisation formelle des systèmes critiques »

Thèmes de recherche :

  • Modélisation des systèmes
  • Spécification et vérification
  • Aspects temporels, coordination des comportements

Sciences du logiciel

Un socle scientifique

  • Modélisation
  • Logique, modèles de calcul
  • Théorie des langages

Des méthodes pratiques

  • Génie logiciel
  • Spécification, vérification
  • Modélisation, programmation

Pour :

  • Concevoir des systèmes : spécifier, modéliser, réaliser, vérifier
  • Maîtriser leur complexité
  • Orientation logicielle, mais spectre large

Sciences du logiciel

SD9, séquence commune à la dominante

  • Droit, éthique et vie privée
  • Eco-conception
  • Programmation et outils de développement
  • Modélisation logique
  • Langages et automates
  • Algorithmique avancée

Outils et concepts indispensables pour la suite de la mention

Sciences du logiciel

Séquences 10 et 11 spécifiques à la mention

  • 420 HEE / 216 HPE en tout
  • Alliance de théorie et de mise en œuvre concrète
  • Évaluation principalement sur projets et bureaux d'étude

Profils ciblés

  • Ingénieurs/chef de projet logiciel en étude ou en R&D
  • Expert/consultant en conception de systèmes logiciels
  • Compétences en génie logiciel, spécification et vérification

Domaines

  • Énergie, transport, défense, santé (systèmes critiques, complexes)
  • Banque, assurance (systèmes d'information)
  • Startups, ESN (développement, modélisation agile)
  • Recherche académique ou industrielle (méthodes de vérification)

Fondements

Comment s'exécute un logiciel ?

  • Principes de fonctionnement des ordinateurs (40 HEE)
    Du transistor à l'interface matériel/logiciel et aux entrées-sorties

Comment fonctionne un compilateur, un interpréteur ?

  • Traitement des langages (30 HEE)
    Grammaires, analyse syntaxique, compilation
  • Ingénierie des modèles et approches génératives (30 HEE)
    Métamodèles, langages spécifiques, interprétation/compilation

Quel sens donner à un modèle ?

  • Logique et systèmes déductifs (40 HEE)
    Comment exprimer une propriété et raisonner sur un modèle
  • Sémantique des modèles et des langages (40 HEE)
    Comment donner un sens précis à un langage ?

Génie logiciel et développement

Comment organiser le développement logiciel ?

  • Génie logiciel (30 HEE)
    Cycles de conception, modélisation objet, patrons de conception

Comment programmer efficacement ?

  • Programmation avancée (30 HEE)
    Critère de choix d'un langage de programmation, idiomes

Comment concevoir et déployer un logiciel distribué ?

  • Algorithmes et modèles pour les systèmes distribués (40 HEE)
    Conteneurs, orchestration de services, stockage de données distribué

Conception de logiciels sûrs

Comment intégrer logiciel et équipements ?

  • Systèmes hybrides (20 HEE)
    Spécificités des interfaces entre logiciel et monde physique

Comment vérifier des logiciels

  • Test (30 HEE)
    Comment tester un logiciel et évaluer la qualité des tests
  • Analyse statique (20 HEE)
    Détecter des erreurs sans exécuter le code
  • Preuve de programme (dans le cours de sémantique)
    Comment prouver des propriétés d'un logiciel

Généralisation hors logiciel

  • Modélisation système (20 HEE)
    Comment appliquer des méthodes de spécification
    et de validation rigoureuses à des systèmes non logiciels

Cours électif (40 HEE)

En séquence SM10

  • Programmation quantique pour le machine learning
  • Développement de systèmes critiques avec la méthode B
  • Spécification et test de systèmes temps-réels
  • SCADE et le synchrone pour les systèmes critiques

Pour approfondir un domaine ou une méthode en particulier.

Que ferez-vous en mention SL ?

De nombreux mini-projets, qui servent à évaluer votre travail :

  • Conception d'un microprocesseur et codage en langage d'assemblage
  • Écriture d'un pilote d'entrées-sorties, gestion des interruptions
  • Écriture d'un mini compilateur Niklaus pour votre microprocesseur
  • Sémantique formelle et preuve de programmes Niklaus (Isabelle/HOL)
  • Analyse statique et preuve de programmes C (Frama-C)
  • Test de programme Java
  • Étude de différents langages, dont Rust
  • Déploiement d'applications avec Docker et Kubernetes
  • Modélisation, langages spécifiques et approches low/no code
  • Modélisation objet, patrons de conception, cycles de développement
  • Application des méthodes formelles à la modélisation système

Plus de détails sur wdi.centralesupelec.fr/infonum-sl/