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.

Assignment

Read the paper I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols by Ma et al. You can also watch the video of the conference presentation of this paper at SOSP 2019, here.

Why are we reading this paper?

What to learn from this paper?

Answer this question

Both I4 and Armada work at the state-machine level, and both are reasoning about concurrent execution (whole computers in I4 and threads in Armada). Could you apply I4's invariant inference to Armada? What might make I4's distributed protocols better suited to invariant inference than Armada's concurrent software?