This course focuses on modeling and specifying computer systems. Students will learn how to reason about the properties and expected behavior of modern software. Topics include designing specifications, property-based testing, model checking, and satisfiability solvers. We will use real-world case studies to motivate the analysis of reliable computer systems. By the end of the course, students will be able to (1) design specifications for the expected behavior of a system, (2) model system behavior using state-of-the-art tools with automated formal methods, and (3) identify and prevent software bugs. While prior experience with algorithm design and analysis is expected, the course will cover any necessary background in systems programming and formal methods.

Units: 1

Max Enrollment: 18

Prerequisites: CS 240 and MATH 225, or permission of the instructor.

Distribution Requirements: MM - Mathematical Modeling and Problem Solving

Typical Periods Offered: Every other year

Semesters Offered this Academic Year: Spring