Reading

We will read and discuss a handful of papers this quarter. Most of the readings are relatively non-technical; they're intended to foster discussion and debate.

Please submit a review for each reading by 5pm on the associated dates below. No late submissions will be accepted for paper reviews.

Your review should have roughly three paragraphs which you can submit on the CSE 505 Spring 2020 Gradescope page:

1. A high-level summary of the paper and a concise recap of its main take-away

2. A description of what you most valued learning from the paper and the paper's greatest strengths

3. A discussion of what you disagreed with or felt could be improved to make the paper stronger

Papers

• Reading 1 : Trusting Trust - Review: April 6, Discussion: April 8

  • • (Optional) Perhaps the shortest paper ever published in a math journal?

• Reading 2 : Social Processes and Proofs of Programs - Review: April 20, Discussion: April 22

  • • Note: this paper exhibits outdated gender norms.

    • (Optional) Read Tony Hoare's classic Proof of a Program: FIND to get a feel for the kind of verification De Millo et al. are arguing against.

    • (Optional) Read Social Processes, Program Verification, and All That for a retrospective response to De Millo et al.

    • (Optional) Read the short back and forth Moshe Vardi had with De Millo and Lipton in the CACM 2010 article More Debate, Please!.

• Reading 3 : Use of Formal Methods at Amazon Web Services - Review: May 4, Discussion: May 6

  • • (Optional) There is also a slightly fancier version of this work that featured in CACM.

• Reading 4 : BP: Formal Proofs, the Fine Print and Side Effects - Review: May 18, Discussion: May 20

  • • (Optional) Read Chapter 1 Sections 1 and 2 from Greg Nelson's highly influential PhD thesis (which is used in the core of all SMT solvers!).

• Reading 5 : Formal Verification of a Realistic Compiler - Review: June 1, Discussion: June 3

  • • (Optional) The "big splash" CompCert paper has more details about an earlier version of the compiler. Note the "mixed-step" semantics!

    • (Optional) Both the Csmith and EMI compiler testing research found many bugs in many C compilers, but no bugs in the verified parts of CompCert.

    • (Optional) CompCert inspired a huge resurgence in formal verification research. For example see the DeepSpec vision document and CACM article.