Course focuses on the formal specification and verification of reactive systems, most notably concurrent and distributed systems. Topics relevant to these systems, such as non-determinism, safety and liveness properties, asynchronous communication or compositional reasoning, are discussed. We rely on a notation (T LA+, the Temporal Logic of Actions) and a support tool (TLC, the TLA+ Model Checker). Students are expected to be knowledgeable in logic and to be able to write symbolic proofs in predicate calculus. A basic understanding of the notions of assertion, precondition, and post-condition is also assumed.

Neural networks are a class of machine learning models which have recently revolutionized many applied machine learning domains such as natural language understanding, image/video processing, bioinformatics, time series analysis. This course teaches students to develop new neural network architectures from scratch and customize them. The course covers all necessary foundations of neural networks including gradient descent optimization and vector calculus. Students will learn how to design models using idioms such as observed variables, latent variables, gate variables and different functions as well as a wide range of state-of-the-art architectures as design examples. Students are expected to have background in data structures.

Explores the main features of modern, high-level, general-purpose programming languages from the user (programmer) standpoint. Students learn how specific features of programming languages can be used effectively in solving programming problems. The course is also an opportunity to use paradigms that expand on simple imperative programming, such as object-oriented, functional and concurrent programming. Students are expected to have background in operating systems fundamentals and Computer organization, and some knowledge of Java.

Master's Project.