This course presents the relational programming paradigm, also called Constraint Logic Programming (CLP), from its logical foundations for programming with mathematical variables and relations in a declarative fashion, to its relevance to symbolic artificial intelligence with various applications in deductive databases, knowledge representation, symbolic computation, combinatorial optimisation, automated deduction and natural language processing.
Prérequis : CSC_2F001_EP; CSC_2F002_EP
Ce cours explore les concepts fondamentaux de la synthèse d'images 2D et 3D. Il couvre de manière générale le rendu, le traitement de la géométrie, la simulation et les images numériques. À travers des projets individuels, vous implémenterez un moteur de rendu 3D complet basé sur la physique en utilisant le lancer de rayons et l'intégration de Monte Carlo, une simulation de fluide reposant sur la géométrie algorithmique, un algorithme de traitement d'images, ainsi qu’un outil de paramétrisation de maillage.
Our society relies on software and hardware systems for both safety- and mission-critical applications (e.g., autonomous vehicles, control systems, device drivers, ...) in different domains (e.g., aerospace, avionics, medical devices, ...). However, designing correct and reliable systems is challenging due to the systems' complexity (e.g., system's size, concurrency, ...). Model Checking studies the theory and algorithms that automatically check if a system always behaves "as intended". Such algorithms are successfully used in real life to verify hardware (e.g., in companies designing hardware like Intel, ARM, Apple, ...) and software (e.g., at NASA, Microsoft, ...).
This course is an introduction to Model Checking and will explain how we can specify a system (e.g., a program, the design of a microprocessor, a distributed protocol) and its properties with a mathematical formalisms (e.g., logic) and how we can reason automatically about all the possible system's executions (e.g., to show that a program or the design of a microprocessor do not contain bugs).
At the end of the course, a student will be able to:
- Model discrete systems (e.g., programs) using formal languages to precisely define the system's executions.
- Express different system properties (e.g., safety, liveness) using temporal logic.
- Reason algorithmically about all the possible executions of a system, deciding if a system satisfies a property.
- Implement the basic model checking algorithms for discrete systems and temporal logic properties.
- Manipulate programmatically state machines, automata, and logical formulas.
- Recognize the challenges of (statically) checking a complex system.
The lectures cover the theoretical aspects of Model Checking, introducing the necessary background, algorithms, and proofs showing the correctness of the approaches. During the tutorials, the students will learn how to implement, in practice, such automated reasoning techniques.
The course focuses on the algorithms for discrete, finite-state systems. It is a starting point for model checking more expressive systems, such as infinite-state systems (e.g., real software), probabilistic systems, timed and hybrid systems (e.g., control systems), and machine-learning systems (e.g., neural networks). The course is also a starting point for exploring other problems in formal methods (e.g., automated program synthesis).
