Reasoning with Big Code

Dino Distefano
Facebook and Queen Mary, University of London, UK


For organisations like Facebook, high quality software is important. Available tools are often lacking in helping programmers develop more reliable and secure applications. Formal verification is a technique able to detect software errors statically, before a product is actually shipped.

In this talk I will describe the reasoning at scale that we do at Facebook, and I will relay some of the experiences of deploying a static analyser that uses logical reasoning and yet works at a velocity consistent with Facebook’s fast-paced engineering culture.