Prerequisites: CSE205 (computer architecture, recommended)
Compilation is the process of transforming high-level programs and abstractions into the binary machine code used in computer processors. This course introduces the principles and techniques of compilation, with parsers, interpreters, and translators, as well as topics in code optimization and semantic analysis. Students will build a compiler for a simple programming language.
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.
Prerequisite: CSC_2F001_EP; CSC_2F002_EP
This course explores fundamental concepts in 2D and 3D computer graphics. It broadly covers rendering, geometry processing, simulation and digital images. Through individual projects, you will implement a full physically-based 3D rendering engine using ray tracing and Monte Carlo integration, a fluid simulation using computational geometry, an image processing algorithm and a mesh parameterization tool.
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 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).
