COSC 69.24 Software Verification: A Survey of Formal Methods

This course introduces formal verification as a practical engineering discipline for building software you can actually trust. Rather than treating formal methods as a high-level academic subject, we study them the way working engineers at AWS, Microsoft, Airbus, and NASA do: as a toolkit for answering the question “is this system actually correct?” and “what are the corner cases we may have missed?” before the system fails in production.

Students progress through three tiers of verification technology: automated model checkers (TLA , Alloy), auto-active verifiers (Dafny), and interactive theorem provers (Rocq, Isabelle). Each tool is grounded in real-world case studies, from the historic Therac-25 radiation therapy tragic accident to AWS’s verification of DynamoDB, so students learn not just how to use each tool, but when to reach for it.

Degree Requirement Attributes

Dist:TAS

The Courses@Dartmouth contains the most up-to-date information about a course. It includes not only the meeting time and instructor, but also its official distributive and/or world culture designation. This information supersedes any information you may see elsewhere, to include what may appear in this ORC/Catalog or on a department/program website. Note that course attributes may change term to term therefore those in effect are those (only) during the term in which you enroll in the course.

Department-Specific Course Categories

Computer Science