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 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?