Lecture preparation

Before lecture, read the paper assigned below, and submit two items to the submission website:

Also keep in mind that you will need to write a paper summary for your choice of papers throughout the semester.


Read the paper Armada: Low-Effort Verification of High-Performance Concurrent Programs by Lorch et al. You can also watch the video of the conference presentation of this paper at PLDI 2020, here.

Why are we reading this paper?

What to learn from this paper?

Answer this question

What non-deterministic choices of a program's execution does Armada encode in the "step object", shown in the paper as σi?