Homework: Reading questions

Submit two items to the submission website (see link in the navigation bar at the top of the page):

Answer the following question:

In the IronFleet paper, what is the spec for an overall system, what is the code that they prove meets the spec, and what is the sequence of arguments (e.g., different types of refinement) that the authors use in their proof? Which of these proof arguments are machine-checked, and which are done on paper?

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.

Creative Commons License