MIT Subject Listing & Schedule
Fall 2025 Search Results

Searched for:

1 subject found.

6.5120 Formal Reasoning About Programs

()
Prereq: 6.1020 and 6.1200
Units: 3-0-9
Lecture: MW2.30-4 (36-156)

Surveys techniques for rigorous mathematical reasoning about correctness of software, emphasizing commonalities across approaches. Introduces interactive computer theorem proving with the Coq proof assistant, which is used for all assignments, providing immediate feedback on soundness of logical arguments. Covers common program-proof techniques, including operational semantics, model checking, abstract interpretation, type systems, program logics, and their applications to functional, imperative, and concurrent programs. Develops a common conceptual framework based on invariants, abstraction, and modularity applied to state and labeled transition systems.
A. Chlipala
Textbooks (Fall 2025)