This talk tells the story of the development of RacerD, a static program analysis for detecting data races that is in production at Facebook. We concentrate here on how the project unfolded from a human point of view. describing twists and its turns in the project, the compromises and design decisions we made to achieve an impactful analysis, and how jumping back and forth between the perspective of an engineer and that of a scientist helped. My aim is to convey what it’s like to work on an open research problem in static analysis, while at the same time pursuing the industrial goal of helping people, and how these two activities can even boost one another.

Peter O'Hearn works as an Engineering Manager at Facebook with the Static Analysis Tools team, and as a Professor of Computer Science at University College London. His research has been in the broad areas of programming languages and logic, ranging from new logics and mathematical models to industrial applications of program proof. With John Reynolds he developed separation logic, a theory which opened up new practical possibilities for program proof. In 2009 he cofounded a software verification startup company, Monoidics Ltd, which was acquired by Facebook in 2013. The Facebook Infer program analyzer, recently open-sourced, runs on every modification to the code of Facebook's mobile apps, in a typical month issuing millions of calls to a custom separation logic theorem prover and resulting in hundreds of bugs being fixed before they reach production.