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:

Yggdrasil has low proof effort because it has cleverly designed abstractions that Z3 can proof correct. But, there are properties of a file system that the Yggdrasil authors cannot model and prove because they rely on Z3. Give one example and explain why.

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