Lecture preparation
Before lecture, read the paper assigned below, and submit two items
to the
submission website:
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
beforehand.
- Submit your answer for the question below, before the beginning of the lecture.
Also keep in mind that you will need to write a
paper summary for your choice of papers
throughout the semester.
Assignment
Read the papers
Lessons from Building Static Analysis Tools at Google
and
Scaling Static Analyses at Facebook.
Why are we reading these papers?
-
More industrial success story.
-
Balance heavy verification with more automated approaches.
-
Read complementary papers to see common themes.
What to learn from these papers?
-
How do the considerations in these papers differ from the other more academic papers we've read?
-
What common themes do you see between the two papers?
-
Understand the relationship between static analysis and the verification we see in research.
Answer this question
What are the specifications that the Google and Facebook static analysis
tools are checking for? What makes it viable for Google and Facebook
to check those specs at large scale, in contrast to more heavy-weight
examples we have seen, such as the Amazon use of formal methods, or the
CompCert compiler?
