Due: Tue, 03 May 2016 09:00:00 -0700
The papers discuss a verified implementation of a replicated key-value store. What is the TCB for this system as implemented in Verdi?
What kinds of composition does Verdi enable (for instance, using VSTs)? What kinds of composition doesn’t it enable?
The papers present examples of specifications both in terms event traces and in terms of the global state of the system. What’s the difference? Which do you prefer? When is one better than the other? Are there other kinds of specifications that could not be easily expressed as either state-based or trace-based?
Provide a list of questions you would like to discuss in class.
Submit a plain text file
with your answers to the questions.