This course is about finding and preventing logical errors in concurrent systems, e.g., programs, hardware devices,controllers. Though formal analysis requires understanding of many theoretical issues, the focus of this course will be on using practical verification tools to analyze interesting examples.

15-899 - Verification of Concurrent, Reactive and Real-Time Programs

This course is a graduate level research seminar on automatic verification techniques for concurrent, reactive, and real-time programs.

17-651 Models of Software Systems

The course shows how different logics can be used to specify properties of software systems, such as functional correctness, dead-lock freedom, and internal consistency. Concepts such as composition mechanisms, abstraction relations, invariants, non-determinism, and inductive and denotational descriptions are recurrent themes throughout the course.

17-654 Analysis of Software Artifacts

18-549 Distributed Embedded Systems

Embedded computers seem to be everywhere, and are increasingly used in applications as diverse as transportation, medical equipment, industrial controls, and consumer products. This course covers how to design and analyze distributed embedded systems, which typically consist of multiple processors on a local area network performing real time control tasks. The topics covered will include issues such as communication protocols, synchronization, real-time operation, fault tolerance, distributed I/O, design validation, and industrial implementation concerns.

18-879 Special Topics in Systems and Controls: Hybrid Systems