CS 845 (01) - Formal Specification and Verification of Software Systems

Formal Spec & Verif of Systems

Durham   Engineering&Physical Sciences :: Computer Science
Credits: 3.0
Term: Fall 2021 - Full Term (08/30/2021 - 12/13/2021)
Grade Mode: Letter Grading
Class Size:   8  
CRN: 12941
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). Prereq: 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.
You must sign up in the Dept Office before registering through WEBCAT.
Instructors: Michel Charpentier

Times & Locations

Start Date End Date Days Time Location
8/30/2021 12/13/2021 TR 9:40am - 11:00am PARS N116