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, based on constraint logic programming (CLP), from its foundations in first-order logic (FOL) making of programming essentially a modeling task using mathematical variables and relations, towards its various applications in symbolic AI, deductive databases, knowledge representation, problem solving, combinatorial optimisation, automated theorem proving, 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).
