MIT Subject Listing & Schedule
IAP/Spring 2021 Search Results

Searched for:

1 subject found.

6.822 Formal Reasoning About Programs

()
Prereq: 6.031 and 6.042
Units: 3-0-9
https://eecs.scripts.mit.edu/eduportal/__How_Courses_Will_Be_Taught_Online_or_Oncampus__/S/2021/#6.822
Lecture: MW2.30-4 (VIRTUAL)

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 (Spring 2021)