Schedule

Classes are listed in the order Fall, Winter, Spring unless otherwise stated.

Course Descriptions

CSE 216: Formal Methods

Formal methods are a set of mathematical techniques for modeling, designing, and analyzing systems to obtain rigorous guarantees about their behavior. These include ways to prove that a system is correct under all possible inputs, or to automatically synthesize correct systems from high-level specifications of what they should do. This course will survey a range of fundamental formal methods techniques for modeling, specification, verification, synthesis, and testing, highlighting applications to hardware and software design, cybersecurity, robotics, autonomous systems, and machine learning. The course will include a project where students will apply formal methods to a problem in a field of their choice. Primary topics we will cover include logical formalisms, SAT/SMT solving, model checking, program synthesis, symbolic execution, and test generation. According to student interest, we will also cover a selection of advanced topics such as modeling of cyber-physical systems, temporal logic falsification, and verification of neural networks.

Prerequisites: No formal prerequisites, but students should be familiar with propositional (Boolean) logic, finite automata, the complexity classes P and NP, and basic graph algorithms. CSE 103 or an equivalent course would be suitable to provide this background.

CSE 101M: Mathematical Thinking for Computer Science

Formulating problems precisely using mathematical concepts, solving mathematical problems, and devising rigorous arguments to back up your claims are essential skills in CS. Students taking upper division courses often need to make rigorous arguments to prove correctness of algorithms/programs and properties of protocols of interaction between compute devices. This course teaches fundamental problem-solving and proof-writing skills, using examples from all areas of CS. In the first half of the course, we study how to formulate and solve mathematical problems arising from CS applications: from small problems, where the main challenge is figuring out how to write them down in formal notation, to large problems requiring you to come up with a plan breaking them into smaller, more tractable steps. In the second half of the course, we study proofs: how to invent the key ideas for your argument, how to build on those ideas to obtain a rigorous proof, and how to write your proof so that it is understandable without losing precision. The course will also instruct students in the use of the typesetting language LaTeX.

CSE 102: Introduction to Analysis of Algorithms

This course covers fundamental techniques for the design and analysis of algorithms. We will discuss how to formally describe an algorithm and rigorously prove it correct, as well as techniques for analyzing the amount of time or memory an algorithm requires. We will study algorithms for core graph and optimization problems that are widely used in practical applications, as well as several general paradigms for designing new algorithms. These include divide-and-conquer, greedy algorithms, and dynamic programming. At the end of the course, students will understand how many of the most important algorithms work, and be able to design and analyze correct and efficient algorithms for new problems.

CSE 103: Computational Models

This course covers mathematical models of computation. These models provide the foundation for the theory of computer science, allowing us to ask and answer questions like "are there problems that computers can’t solve?" The concepts and algorithms we will study also underlie many areas of computer science practice, e.g. textual search, compilers, and constraint solvers. We start with finite automata and regular languages, studying their expressiveness as well as algorithms for manipulating them. We do the same for the more powerful models of pushdown automata and context-free languages. In the second half of the course, we study Turing machines, a model of general computation. We will explore computability theory, which examines which problems can be solved by algorithms, as well as complexity theory, which examines what resources are needed to solve computational problems.