Welcome to the Fall 2020 web page for CS524

Contact Information

For any course-related issues, plese send an email to:


Please do not send email to the instructor's email account: use only the above email.  If you need to contact

the instructor in any other way, please send email to the instructor's administrative assistant, Ms. Allison Mette:


Zoom link for first lecture [Aug. 25]


Zoom link for lectures on Thursdays [Aug. 27 to Dec. 3]


Zoom link for lectures on Tuesdays [Sept. 1 to Dec. 8]


Course Syllabus

The course will cover the following topics, roughly
in the order listed below:

  1. Logics and Models of Concurrency
    These will include: Rewriting Logic, Petri Nets, the Pi Calculus and
    other Process Calculi, The Actor Model, and Concurrent Versions of
    the Lambda Calculus and Combinatory Logic.
  2. Formal Semantics of Concurrent Programming Languages
    This will include both Operational and Mathematical Semantics
    of declarative and Imperative Concurrent Programming Languages.
  3. Model Checking and Deductive Verification of Concurrent Systems
    Model Checking will discuss:
    (1) temporal logics beyond LTL, with explicit support of actions and fairness assumptions;  
    (2) simulation, bisimulation, and abstraction techniques;
    (3) symbolic model checking of infinite-state systems.
    Deductive Verification Approaches will cover verification of
    properties in Reachability Logic, Hoare Logic and Separation Logic.
  4. [If time permits]  Formal Specification and Verification of
    Concurrent Real-Time and Probabilistic Systems.

Course Work, Policies and Procedures

Students taking the course will be expected to:

  1. Participate actively and regularly in the course.
  2. Study, and sometimes present, some research papers,
     either individually or as part of a small group.
  3. Develop a term project, either individually or as part
     of a small group.

The regularity in active participation and the quality of understanding in the
presentation of papers will contribute 40% to the final grade.  The quality of
the term project will contribute the remaining 60%.  There will be no final exam.

Learning Outcomes

After successfully taking this course, a student will understand the
basic notions of concurrency theory as well as the various logics and
models used in concurrency.  These concepts will then be applied to
the mathematical and operational semantics of concurrent programming
languages.  The student will also learn how formal reasoning about the
correctness of concurrent systems and programs in concurrent languages
can be supported by various property logics and by both automatic
verification methods based on model checking and interact methods
based on theorem proving.  Furthermore, the course will serve as
a preparation to understand and use the current literature on
concurrency theory, semantics of concurrent languages, and
verification of concurrent systems.

Maude Language Web Site


Lecture Notes