Week 9 Static Analysis Tutorial

Activity

Read the papers Lessons from Building Static Analysis Tools at Google and Scaling Static Analyses at Facebook.

Why are we reading these papers?#

  1. More industrial success story.
  2. Balance heavy verification with more automated approaches.
  3. Read complementary papers to see common themes.

What to learn from these papers?#

  1. How do the considerations in these papers differ from the other more academic papers we’ve read?
  2. What common themes do you see between the two papers?
  3. Understand the relationship between static analysis and the verification we see in research.

Answer the following questions

  1. What are the specifications that the Google and Facebook static analysis tools are checking for?
  2. What makes it viable for Google and Facebook to check those specs at large scale, in contrast to more heavy-weight examples , such as the Amazon use of formal methods, or the CompCert compiler?

References

[1] CMU Tutorials: https://cmu-313.github.io/recitations/

bars search times arrow-up