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 Formal Proofs, the Fine Print and Side Effects by Murray et al.

Why are we reading this paper?

What to learn from this paper?

Answer this question

In Figures 2-5, the paper presents Venn diagrams showing possible changes to the system's code. Thinking about these diagrams from the perspective of the lab assignments in this class, where do you think your code changes lie? Did formal verification force you to fix bugs (P and A)? Did formal verification force you to make irrelevant changes (P but not A)? Were there any bugs you introduced during verification (V) or issues you realized were there but not required for formal verification (A but not P)? What are the most interesting examples of these bugs from your experience?