Teachings

École polytechnique : Formal Methods Track

Formal Methods and Foundations of Cyber-Physical Systems

Formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. These methods have advanced deep logical and mathematical topics, including abstract interpretation, proof methods and assistants (as well as higher-order logical frameworks such as Coq, Agda, and Lean), model checking, and SAT/SMT algorithms, all of which are central to this track. This includes all relevant semantic and algorithmic aspects.

Télécom SudParis : Complex Networks

Automata based approaches

Contenus du cursus 1 : Grands Graphes, systèmes complexes, réseaux sociaux, graph du web, diffusion de l’information dans les grands graphes

• Lois de d’échelle
• Rappel de théorie des graphes
• Graphes aléatoires
• Propriétés statistiques remarquables des grands graphes de terrain (graphe du web) : Effet petit monde, Lois d’échelle dans les grands graphes, Modélisation des grands graphes, Structure de l’internet
• Détections de communautés dans les graphs graphes de terrain : Application aux réseaux sociaux en ligne
• Navigation dans les graphes (Algorithme du PageRank)
• Robustesse des grands systèmes : Panne en cascade, Robustesse de l’Internet
• Mécanismes de diffusion de l’information dans les graphes (modélisation épidémie, Marketing virale dans les réseaux sociaux)

Contenus du cursus 2

• Aperçu Test vs vérification
• Modélisation et abstraction des systèmes du monde réel
• Des systèmes aux mots, traces et langages
• Réduction des expressions régulières en automates finis (2, p)
• Tour d'horizon des méthodes formelles
• Assistants de preuve formelle
• Analyse de code
• Systèmes concurrents et distribués
• Exécution séquentielle vs exécution concurrente
• Horloges de Lamport et relation « happens-before »
• Partage des ressources et exclusion mutuelle (2, p)
• Protocoles de validation et autres algorithmes distribués (3, p)
• Conception, raffinement et implémentation
• Implémentation d'une conception (2, p)
• Composition des sous-systèmes (3, p)

ENSTA : 0ptimal control & hybrid systems

Mario Gleirscher, Associate Professor of the ASC Chair at ENSTA, has introduced two new courses that have been integrated into the school's engineering program. Below is the description of the first course :

Course Title: Hybrid Systems and Optimal Control for Reliable Automation

Objective: To use theories, models, and techniques from hybrid systems and optimal control to design controllers with guarantees. These controllers are essential for reliably performing complex tasks in high-automation domains, such as autonomous robotics.

Learning Goals: By the end of this course, students will be able to :

   Describe complex system dynamics using hybrid system models.
   Examine such models (e.g., simulate, evaluate, verify) using analytic and numerical techniques.
   Design and synthesize correct controllers based on these models.
   Utilize optimization algorithms and tools to facilitate controller synthesis.
   Apply hybrid system models, techniques, and tools to simple examples.

The ASC Challenge : a response to the Chair’s commitment to promote Complex Systems Architecture.
The ASC Challenge reflects the Chair’s goal of disseminating Complex Systems Architecture in a transversal and unified manner across the schools of the Institut Polytechnique de Paris.

Objective : this challenge aims to provide participating students with knowledge and skills in the following areas:

   Complexity;
   Systems thinking;
   Systems of Systems (SoS) approaches;
   Model-Based Systems Engineering (MBSE);
   Comparison and evaluation of SoS architecture variants.

To access the challenge platform, click here.