Durham
Engineering&Physical Sciences :: Computer Science
CS 845 (01) - Formal Specification and Verification of Software Systems
Formal Spec & Verif of Systems
Credits: 4.0
Term: Fall 2024 - Full Term (08/26/2024 - 12/09/2024)
Grade Mode: Letter Grading
Term: Fall 2024 - Full Term (08/26/2024 - 12/09/2024)
Grade Mode: Letter Grading
Class Size:
10
CRN: 16265
CRN: 16265
Course focuses on the formal specification and verification of reactive systems, most notably concurrent and distributed systems. Topics relevant to these systems, such as non-determinism, safety and liveness properties, asynchronous communication or compositional reasoning, are discussed. We rely on a notation (T LA+, the Temporal Logic of Actions) and a support tool (TLC, the TLA+ Model Checker). Students are expected to be knowledgeable in logic and to be able to write symbolic proofs in predicate calculus. A basic understanding of the notions of assertion, precondition, and post-condition is also assumed.
Registration Approval Required. Contact Instructor or Academic Department for permission then register through Webcat.
Cross listed with : CS 745.01
Instructors: Michel Charpentier
Start Date | End Date | Days | Time | Location | |
---|---|---|---|---|---|
8/26/2024 | 12/9/2024 | TR | 9:40am - 11:00am | KING N133 | |
Final Exam | 12/11/2024 | 12/11/2024 | W | 10:30am - 12:30pm | KING N133 |