Course Number
605.729
Next Offered
Spring 2024
Primary Program
Computer Science
Location
Online
Course Format
Virtual Live

All science requires mathematics. Formal methods used in developing computer systems are mathematically based techniques for describing system properties. These formal methods then can provide frameworks within which developers can specify, develop, verify, and prove systems in a systematic, rather than ad hoc manner. According to some researchers, the application of formal specification and verification methods could avoid disasters such as Heartbleed bug, Ariane 5 rocket explosion, and Therac-25 radiation therapy machine harms. This course is an introduction to the vast world of formal methods. The course starts with review of propositional logic, predicate logic, and covers set theoretic specification methods via Z, temporal specification via PTL, grammars, and logic based methods via Caml and Coq proof assistant. Each student will carry out an investigation of an existing formal verification system, applying it to a suitable problem of the student’s choice. Among possible projects will be the formal verification of problem solutions such as designing a semaphore, designing a machine learning algorithm, a web interface, a test suite, a sophisticated data structure, or a theorem.

Course Offerings

Open

Formal Methods

605.729.8VL
01/22/2024 - 04/29/2024
Mon 4:30 p.m. - 7:10 p.m.
Notes: This course uses the Virtual Live format. All students participate online through live web-conferencing at the scheduled day and time. This is a live-online course in which students participate in live weekly lectures and discussions, and are able to interact extensively with the instructors. All classes are recorded for download and review.
Semester
Spring 2024
Course Format
Virtual Live
Location
Online
Cost
$5,090.00
Course Materials