Lecture preparation
Before lecture, read the paper assigned below, and submit two items
to the
submission website:
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
beforehand.
- Submit your answer for the question below, before the beginning of the lecture.
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
Scaling symbolic evaluation for automated verification of systems code with Serval
by Nelson et al.
Why are we reading this paper?
What to learn from this paper?
Answer this question
Serval requires systems to have “finite interfaces” for automated
verification. Recall the lectures on CertiKOS and Komodo. Is any
interface operation in the CertiKOS/Komodo non-finite? If yes, describe
one example; otherwise, design a non-finite operation. How would you
break this non-finite operation into smaller, finite operations to make
verification easier?
