Reasoning with Big Code
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
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.