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

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.