CS 4830 — System Specification, Verification, and Synthesis

4 semester hoursUndergraduateLecturetypical days: M/W/ThBostonTraditional

Covers the fundamental topics in formal modeling and specification (transition systems, temporal logic, regular and omega-regular languages, safety and liveness properties, etc.); computer-aided verification (state-space exploration, model checking, bounded-model checking, binary-decision diagrams, symbolic model checking, etc.); compositionality and assume-guarantee reasoning; contracts; and component-based design. Also covers fundamental topics in computer-aided synthesis of correct-by-construction systems, starting from high-level formal specifications or from example scenarios. Designing large and complex systems (digital circuits, embedded control systems such as automated vehicles, computerized healthcare devices such as pacemakers, cyber-physical systems such as automated intersections, etc.) and their software cannot be done by hand. Instead, designers use computer-aided techniques that allow them to build system models and verify correctness of the design before the real system is actually built.

Prerequisites

Offering history

TermSectionsEnrolledCapacityFullOpen seats/section
Fall 202316875%2.0
Spring 2026122010%18.0

Snapshots from scheduled scrapes — not live seat availability. "Full" can exceed 100% when sections over-enroll.

Meeting times

Share of recent sections by weekday: M 100% · T 0% · W 100% · Th 75% · F 0%

Common patterns: MWR (75% of sections), MW (25% of sections) — in patterns, R means Thursday

Professors

Fall

Spring

Percentages are each professor's average share of the season's enrolled students in recent terms.

Links

Official catalog (CS course descriptions) · Student reviews on RateMyHusky · All CS courses · Plan it at numap.app