Les enseignements de la chaire ASC

Formal Methods and Foundations of Cyber-Physical Systems (FM track):

Formal methods are mathematically rigorous techniques for the specification, development, analysis and verification of software and hardware systems. Formal methods have developed deep logical and mathematical subjects such as abstract interpretation, proof methods and assistants (and higher-order logical frameworks such as Coq, Agda, Lean), model-checking and SAT/SMT algorithms, which are at the core of this track, with all the relevant semantic and algorithmic aspects.

The 5 core courses of the track among which the students should choose at least 3, provide all the necessary theoretical and practical material for proof assistants (CSC_51051_EP, Ambroise,CSC_52003_EP), abstract interpretation (CSC_51075_EP) and model-checking, SAT/SMT (CSC_51075_EP, Jeremy) with various application domains in mind: program proofs and synthesis (CSC_51051_EP, Ambroise, CSC_51075_EP, CSC_52003_EP), and validation of cyber-physical and AI based systems (CSC_51075_EP, Jeremy).

Formal methods had great success stories in designing correct systems, or finding bugs. For instance, formal methods have been instrumental in the design of the autonomous metro lines of RATP (e.g. line 14) and they are part of international standards for aeronautics such as DO178C. Formal methods have been included in the continuous development of operating systems and drivers at Microsoft - developing such tools as the SMT solver Z3 or the logical framework TLA+ for designing and proving concurrent and distributed systems. Intel has used formal methods since the discovery of the FDIV Pentium bug in 1994 and Amazon AWS systematically uses formal methods for the design and verification of its cloud services, used by 4.19 million customers worldwide in 2025.

There are now a wealth of interactions of formal methods with other branches of mathematics and computer science, that are reflected in the program of this track:

   Logics and algorithmics: most properties of interest are undecidable, but some fragments or some abstractions lead to algorithmically tractable methods. SAT/SMT are the prototype NP-complete problems but heuristics allow for practical applications at scale. Quantum computing has non-intuitive mathematical semantics and algorithmics and needs specific verification techniques for proving correctness (complements you may want to take are then e.g. INF555, INF550, MDC_51005_EP,INF560, INF571, CSC_52003_EP)

   AI based systems are in dire need for formal methods, enhancing the confidence that users can have in such systems, by proving robustness of decisions (against e.g. adversarial attacks), privacy and fairness properties, explainability etc. (complements you may want to take are e.g. INF554, MAP553, MAP555, INF581, INF581a)

   Cyber-physical systems (distributed control systems), potentially powered by AI, are systems which interact with the physical world: autonomous cars and transportation systems, smartgrid, swarms of drones, medical apparatus etc. Bugs or failure to comply with specifications may induce huge financial losses or even kill customers, meaning that formal proofs are of great interest to this field (complements you may want to take are e.g. INF559, INF563, INF558, INF565, INF568, INF571)

Mots-clés : Grands Graphes, systèmes complexes, réseaux sociaux, graph du web, diffusion de l’information dans les grands graphes.
Contenu
Réseaux Complexes:
1) Lois de d’échelle
2) Rappel de théorie des graphes
3) Graphes aléatoires
4) Propriétés statistiques remarquables des grands graphes de terrain (graphe du web)
a) Effet petit monde
b) Lois d’échelle dans les grands graphes
c) Modélisation des grands graphes
d) Structure de l’internet
5) Détections de communautés dans les graphs graphes de terrain
a) Application aux réseaux sociaux en ligne
6) Navigation dans les graphes (Algorithme du PageRank)
7) Robustesse des grands systèmes
a) Panne en cascade
b) Robustesse de l’Internet
8) Mécanismes de diffusion de l’information dans les graphes (modélisation épidémie, Marketing virale dans les réseaux sociaux)
Lien cursus 1

1 Overview Testing vs. Verification
1.1 Modelling and abstracting real-world systems (1)
1.2 From systems to words, traces and languages (1)
1.3 Reduction of regular expressions to finite automata (2, p)
2 A tour through the landscape of formal methods (1)
2.1 Automata based approaches (1, 2)
2.2 Formal Proof Assistants (1)
2.3 Code analysis (1)
3 Concurrent and distributed systems
3.1 Sequential vs Concurrent execution (2)
3.2 Lamport clocks and happens-before relation (2)
3.3 Resource sharing and mutual exclusion (2, p)
3.4 Commit protocols and other distributed algorithms (3, p)
4 Design, refinement and implementation
4.1 Implementing a design (2, p)
4.2 Composition of sub-systems (3, p)
Lien cursus 2

Management prédictif des accumulateurs

Participation au challenge "Swarm rescue" du CIEDS

Modélisation : travail sur la partie neurosymbolique

Modélisation : travail sur la partie symbolique

Participation au challenge UAV de Dassault Aviation

Participation au challenge UAV de Dassault Aviation

Sujet de physique sur les systèmes de navigation
Tuteur Naval Group

Participation au challenge "Swarm rescue" du CIEDS

Challenge ASC 2025 : 9 équipes d'étudiants conçoivent un système de systèmes de défense, tutorés par les partenaires ASC

Lien vers le challenge

Sujet d'informatique sur le calcul de trajectoire
Tuteur Dassault Aviation

Sujet d'informatique sur les jumeaux numériques de structure
Tuteur Dassault Aviation

Création d'un scénario d'anticipation de défense sur le mode de la RedTeam défense de l'AID (Saison 2)
Blue Team : DGA & AID
Tutorat ASC

Participation au challenge UAV de Dassault Aviation

Sujet de physique sur le givrage
Tuteur Dassault Aviation

Sujet de physique sur les trainées de condensation
Tuteur Dassault Aviation

Participation au challenge UAV de Dassault Aviation

Participation au challenge UAV de Dassault Aviation

Participation au challenge "Swarm rescue" du CIEDS

Participation au challenge "Swarm rescue" du CIEDS

Participation au Challenge UAV de Dassault Aviation
Lien post

Création d'un scénario d'anticipation de défense sur le mode de la RedTeam défense de l'AID
Blue Team : DGA & AID
Tutorat ASC
Lien post
Lien vidéo
Lire le scénario