CS524

Welcome to the Fall 2020 web page for CS524

Contact Information

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

cs524-staff@illinois.edu

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:

agk@illinois.edu

Zoom link for first lecture [Aug. 25]

https://illinois.zoom.us/j/93353132966?pwd=Lys4RGpsMEdYRXlEOVJmTzh5ZnI5dz09

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

https://illinois.zoom.us/j/99738360903?pwd=ejEzdk05OEMvR0FTMVNPYlp4dUU2Zz09

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

https://illinois.zoom.us/j/96003751168?pwd=VDBpM2tiaElMR2xRZ200Ymx3TFROUT09

Course Syllabus

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

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.
Formal Semantics of Concurrent Programming Languages
This will include both Operational and Mathematical Semantics
of declarative and Imperative Concurrent Programming Languages.
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.
[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:

Participate actively and regularly in the course.
Study, and sometimes present, some research papers,
either individually or as part of a small group.
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

http://maude.cs.uiuc.edu

Lecture Notes