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