Infer,[1] sometimes referred to as "Facebook Infer", is a static code analysis tool developed by an engineering team at Facebook along with open-source contributors. It provides support for Java, C, C++, and Objective-C, and is deployed at Facebook in the analysis of its Android and iOS apps (including those for WhatsApp, Instagram, Messenger and the main Facebook app).[2]
Infer has its roots in academic research on Separation Logic, a theory for the formal verification of software. Work on automatic program verification based on Separation Logic led to a succession of academic tools, including Smallfoot and SpaceInvader. Building on the academic work, Cristiano Calcagno, Dino Distefano and Peter O'Hearn, three researchers at University College London and Queen Mary University of London, co-founded the verification startup Monoidics in 2009, and Monoidics developed the first version of Infer.[3][4][2] Monoidics was acquired by Facebook in 2013,[5] and in 2015 the code of Infer was open-sourced.[2][6]
As of 2013 when Infer was open-sourced it was claimed that hundreds of bugs per month identified by Infer were fixed by Facebook's developers before reaching production.[5] By 2015 this had increased to over 1000 bugs per month.[7]
Spotify, Uber, Mozilla, Sky, and Marks and Spencer are among the reported users of Infer.[1]
Infer performs checks for null pointer exceptions, resource leaks, annotation reachability, missing lock guards, and concurrency race conditions in Android and Java code. It checks for null pointer problems, memory leaks, coding conventions and unavailable API's in C, C++ and Objective C.[1]
Infer uses a technique called bi-abduction[8] to perform a compositional program analysis that interprets program procedures independently of their callers. It is claimed that this enables Infer to scale to large codebases and to run quickly on code-changes in an incremental fashion, while still performing an inter-procedural analysis that reasons across procedure boundaries.[9]
Infer is wired up to the code review system at Facebook. Its deployment model is to comment automatically on code modifications as they are submitted for review, where it reports potential regressions. It does this by incrementally analyzing code changes via a job on Facebook's continuous integration system which runs in its data centers.[9]
Infer also has a domain specific language for abstract syntax tree linting, based on ideas from Model Checking for Computation Tree Logic.[10] [11]
Infer is mostly written in the OCaml programming language.[12]
Dino Distefano [it] received the Royal Academy of Engineering silver medal in 2014 in recognition of the acquisition of Monoidics.[13]
Four Infer team members, Josh Berdine, Cristiano Calcagno, Dino Distafano and Peter O'Hearn, received the 2016 Computer Aided Verification Award, an award they shared with John C. Reynolds, Samin Ishtiaq and Hongseok Yang.[7][14]
Peter O'Hearn was elected Fellow of the Royal Academy of Engineering in 2016, for his work on Separation Logic and Infer.[15]