Infer is an open-source static analyser that is used to find bugs in code at Facebook. Every month, Infer runs on thousands of code changes and detects thousands of bugs that are fixed by developers before they reach production.
Over the years, Infer has evolved from a standalone separation logic-based analyser to a powerful framework for quickly implementing modular interprocedural analyses. This framework can take a simple intraprocedural analysis that computes the summary for a single procedure and lift it to a compositional interprocedural analysis that scales to millions of lines of code. Because of compositionality, the analysis can run much more quickly on a code change than on an entire codebase, opening the way to a “move fast” form of deployment which keeps pace with the workflow of developers. Infer analyses target a common intermediate language, which allows each analyser to be run on Java, C++, Objective-C, and C code with minimal language-specific logic.
The goal of this tutorial is to explain the capabilities of this framework and encourage attendees to use Infer as a platform for their own research. Attendees will learn tips and tricks for compositional program analysis at scale and gain hands-on experience in writing new analyses using the Infer infrastructure.