M1 MPRI at ENS Paris-Saclay: Course Catalogue

WIRE: Initiation to Research Workshop

Objectives: The aim of this module is to develop—through hands-on practice—skills specific to research work. These skills include: assessing the state of the art in a given problem or field, formulating a research problem, presenting research findings to colleagues, identifying the key aspects of a research field (significance, motivation, applications, and future prospects), and mastering the professional standards of the research community. Workshops are organized in groups of 6 to 8 students, led by a faculty researcher or senior researcher. Participants are assigned tasks on a weekly basis, and independent work is required between sessions.

More...

ADCO: Advanced Complexity

Objectives: Complexity theory extends well beyond the concept of NP-completeness. The aim of this course is to examine a number of other fundamental constructs in complexity theory, such as space complexity and the concepts of alternating or randomized machines. We will explore some fascinating theorems, for instance, the equivalence between alternating time and deterministic space, or Shamir's IP=PSPACE theorem.

More...

AFIT: Algorithms for Formal Calculus and Information Theory

Objectives: The aim of this advanced algorithms course is to teach efficient algorithms related to effective algebra and information theory. More specifically, we will study operations on polynomials and large integers, error-correcting codes, and data compression.

More...

CBIO: Computational Bio-engineering

Objectives: Bioengineering is a rapidly growing discipline with applications in bioproduction, pharmaceuticals, environmental science, and medicine. It draws on expertise from biology, computer science, control theory, and other fields. Upon completion of this course, students will be able to:

• Construct and use mathematical models for bioengineering.
• Apply compilation, control, and optimization techniques to a biological process.
• Analyze and utilize experimental data from spectroscopy and microscopy.

More...

DONA: Distributed and Online Algorithms

Objectives: This advanced algorithms course aims to provide a foundation in probability as applied to classical and online algorithms, as well as the principles of distributed algorithms. Upon completion of this course, students will be able to: (1) Analyze randomized algorithms by examining their expected execution time and error probability. (2) Explain and apply competitive analysis to online algorithms. (3) Understand the fundamentals of reasoning about distributed algorithms and their constraints.

More...

ICAT: Introduction to Categories

Objectives: One focus of category theory is on studying relationships between structures occurring in mathematics and the foundations of computer science. Instances of abstract categorical concepts appear in many different fields, to which general categorical theorems can then be applied. For instance, the basic categorical concept of a "binary product" can be instantiated in the category of sets (cartesian product), in the category of vector spaces (direct sum), and in any poset (meet). Similar remarks apply to, among others, the categorical concepts of "functor", "natural transformation", and "monad". Category theory thus provides a useful level of abstraction for proving generic results. Moreover, categories themselves can also be used as models for logics and type theories. This establishes a strong back-and-forth connection between category theory, logic, and programming languages: the Curry-Howard-Lambek correspondence. For instance, the category-theoretic notion of "monad" was exported to functional programming languages such as Haskell. Categorical methods also feature prominently in research on the semantics of dependently typed languages (such as Agda, Lean, and Rocq) and have been used also in the context of quantum computing. Finally, during the course we may also mention some connections between category theory and automata theory.

More...

IVER: Introduction to Verification

Objectives: The course provides an introduction to model-checking techniques used to verify the reliability of critical systems. It begins with the modeling of discrete-event systems—transition systems augmented with data structures for communication (variables, messages) and various synchronization methods. Next, we examine temporal logics (linear and branching-time) for expressing properties to be verified, specifically LTL, CTL, and CTL*. We study their expressiveness, decidability, and the complexity of associated problems.

The second part of the course focuses on advanced methods to address the state-space explosion problem. In particular, we cover Binary Decision Diagrams (BDDs), partial-order reduction, and counterexample-guided abstraction refinement, as well as the concepts of simulation and bisimulation. While the majority of the course deals with the verification of finite-state systems, we also introduce model checking for infinite-state systems by studying Petri nets and pushdown automata.

More...

LIAK: Logic for AI: Knowledge Logics

Objectives: This course focuses on the logical aspects of artificial intelligence, aiming to reason formally about the knowledge held by agents or coalitions of agents. The methods presented in the course are derived from foundations in logic and automata theory, as well as from the model-checking approach used for program verification. Several families of logical formalisms are introduced, including description logics (such as ALC), strategic temporal logics (such as ATL), and similar formalisms.

More...

PACS: Probabilistic Aspects of Computer Science

Objectives: The aim of this course is to introduce the main models for discrete-event systems (Markov chains, Markov decision processes, probabilistic automata), along with their underlying theory and associated algorithms. It also covers random graph theory—a framework particularly well-suited to modeling large-scale distributed systems such as telecommunication networks or social networks. This course prepares students for the courses within the "Automata/Games" track of the MPRI Master's program (second year).

More...

PROT: Proof Theory

Objectives: In a mathematical proof, one can distinguish between steps of reasoning and steps of calculation. This course aims to provide a general framework for expressing these two aspects and to introduce the basic tools needed to verify key properties of the calculation rules employed (such as termination, confluence, and models). It also provides an introduction to dependent types and how they can be used to represent formulas and proofs from various logics in a modular fashion.

More...

TAIG: Tools for AI: Game theory

Objectives: This course offers an introduction to the fundamental concepts of game theory, designed for computer science students. It focuses on key models and solution concepts, as well as their algorithmic aspects. The course covers strategic-form games, extensive-form games, and games on graphs.

Connections to artificial intelligence are illustrated through topics such as adversarial search, learning in games, game solving, and reinforcement learning. The course also provides the game-theoretic foundations necessary for subsequently taking the Mechanism Design course.

More...

TAIS: Tools for AI: Solvers

Objectives: This course introduces the key tools of automated reasoning, a field aimed at automatically learning and generating new knowledge based on a logical representation of systems. The course covers algorithms for deciding the satisfiability of formulas within various fragments of first-order logic—such as propositional logic, equality constraints between terms, and linear arithmetic over reals and integers—which are used in program verification and synthesis. It also examines the combination of these algorithms via the Nelson-Oppen principle, as well as constraint programming. Theoretical concepts will be applied to problem-solving using existing tools (CVC, Z3) and to the implementation of new decision procedures.

More...

ACOM: Advanced Compilation

Objectives: This course is an introduction to compilation. It explains the techniques and tools used in the different phases of a compiler, up to the production of optimized assembly code.

More...

APSA: APproximation and String Algorithms

Objectives: This advanced algorithms course aims to introduce students to the fundamentals of string algorithms, approximation algorithms, and linear programming. The concepts covered include the design of efficient algorithms for classic problems and approximation problems, as well as applications of linear programming techniques.

More...

ADSE: ADvanced Software Engineering

Objectives: This course introduces methodologies for software application development that are independent of the chosen programming language. These methods enable the capture of user requirements, application design at a language-independent level, team coordination, error prevention, detection and correction, code maintainability, and the delivery of a robust software product. The lessons will cover the fundamentals of modeling, design, and rigorous software development, as well as testing methods and version control. Students will apply these methodologies through a group project (groups of 3 to 6). In the first stage, students will select a topic from the options provided, complete the requirements specification, and propose a detailed application design. In the second stage (second period), they will develop the project and validate it using the techniques they have learned. Project assessment will take into account all aspects of the project: design, coding, validation, work coordination, documentation, and the final software product.

More...

NETS: Networks

Objectives: This module introduces key concepts in computer networking, such as addressing, data exchange, routing, and transport protocols. It takes a formal approach, illustrating these concepts using models such as message sequence diagrams and communicating automata. The module also covers socket programming and includes a project involving the development of a distributed application.

More...

ISEC: Security

Objectives: This module introduces the modeling and verification of cryptographic protocols. Regarding modeling, the course will present a process algebra for representing sets of communicating agents, as well as a language for expressing security properties—such as authentication, data secrecy, and anonymity—expected of cryptographic protocols. It will also cover symbolic abstractions of cryptography (specifically, the Dolev-Yao model) and decision or semi-decision procedures for verifying the security of certain classes of protocols. Finally, the course will briefly introduce reduction-based proof techniques applicable when cryptography is not abstracted (i.e., within the computational model).

More...

OMD: Mechanism design

Objectives: This course studies the design of mechanisms to mediate the interaction of strategic individuals so that desirable outcomes are attained. A central theme will be the tradeoff between optimality of an objective such as revenue or welfare and other desirable properties such as simplicity, robustness, computational tractability, and practicality. This tradeoff will be quantified by a theory of approximation which measures the loss of performance of a simple, robust, and practical approximation mechanism in comparison to the complicated and delicate optimal mechanism. The class focuses on techniques for performing this analysis, economic conclusions, and consequences for practice.

More...