Cristiano Calcagno, Dino Distefano, and Peter W. O’Hearn (three of the Facebook engineers behind Infer) and Hongseok Yang of KAIST received this year’s ACM SIGPLAN Most Influential POPL Paper Award. Their paper, “Compositional Shape Analysis by Means of Bi-abduction,” described techniques used in developing Infer, Facebook’s static program analyzer, which was open-sourced in 2015.
At Facebook, we use Infer to scan source code to detect possible bugs before that code is shipped. Every change made to our mobile code is checked by Infer. Unlike most other static analyzers, Infer performs sophisticated interprocedural and interfile analysis at scale. It can detect subtle bugs by tracking values through many procedure calls or where the procedures live across different files. Although sophisticated and deep, Infer’s analyses scale well to large programs consisting of millions of lines of code. Each month, thousands of potential bugs identified by Infer are fixed by our engineers before they are committed to our codebases and deployed to people’s phones. This saves our engineers many hours of finding and fixing bugs, and results in better products for people.
In 2017, members of this team introduced AL, a simple declarative language that allows any engineer to easily design new checkers without any knowledge of Infer’s inner workings. They also described how Infer detects interprocedural bugs and expanded its use to detect concurrency bugs at scale, and to apply to multithreaded rendering. Both Infer and AL have been open-sourced and are in use at several large tech companies, including Amazon, Mozilla, and Spotify.
For more about the winning paper and how it led to Infer, read the Q&A with the authors on research.fb.com.
