Abstract

Infer is an open-source static analysis platform that is used to prevent classes of bugs in code at Meta in several languages such as Java, C++, or Hack. 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 analyser based on Separation Logic to a powerful platform for implementing cross-language interprocedural analyses. Static analysis writers only need to provide an intraprocedural analysis that computes the summary for a single procedure and Infer will transform it into a compositional interprocedural analysis that scales to millions of lines of real code. In this talk, we’ll go through some of the formal methods techniques that are implemented inside Infer such as separation logic, abstract interpretation, and incorrectness logic, and how they make it a valuable tool for programmers.