Infer, 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).
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 in London, co-founded the verification startup Monoidics in 2009, and Monoidics developed the first version of Infer. Monoidics was acquired by Facebook in 2013, and in 2015 the code of Infer was open-sourced.
As of 2013 when Infer was open-sourced it was claimed that 100s of bugs/month identified by Infer were fixed by Facebook's developers before reaching production. By 2015 this had increased to over 1000 bugs/month.
Spotify, Uber, Mozilla, Sky, and Marks and Spencer are among the reported open source users of Infer.
Video Infer Static Analyzer
Technology
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.
Infer uses a technique called bi-abductionto 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.
Infer is wired up to the code review system at Facebook. It's 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.
Infer also has a domain specific language for abstract syntax tree linting, based on ideas from Model Checking for Computation Tree Logic.
Infer is mostly written in the OCaml programming language.
Maps Infer Static Analyzer
Awards
Dino Distefano received the Royal Academy of Engineering silver medal in 2014 in recognition of the acquisition of Monoidics.
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 Reynolds, Samin Ishtiaq and Hongseok Yang.
Peter O'Hearn was elected Fellow of the Royal Academy of Engineering in 2016, for his work on Separation Logic and Infer.
References
Source of article : Wikipedia
0 Comments