Infer Static Analyzer

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]

History

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.[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]

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.[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]

Awards

Dino Distefano 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]

References
  1. "Infer static analyzer". Website.
  2. Calcagno, Cristiano; Distefano, Dino; O'Hearn, Peter. "Open Sourcing Facebook Infer: Identify Bugs Before You Ship".
  3. Calcagno, Cristiano; Distefano, Dino; O?Hearn, Peter W.; Yang, Hongseok (1 December 2011). "Compositional Shape Analysis by Means of Bi-Abduction". Journal of the ACM. 58 (6): 1–66. CiteSeerX 10.1.1.420.2150. doi:10.1145/2049697.2049700.
  4. Calcagno, Cristiano; Distefano, Dino (18 April 2011). Infer: An Automatic Program Verifier for Memory Safety of C Programs. NASA Formal Methods. Lecture Notes in Computer Science. 6617. Springer, Berlin, Heidelberg. pp. 459–465. CiteSeerX 10.1.1.421.9629. doi:10.1007/978-3-642-20398-5_33. ISBN 978-3-642-20397-8.
  5. Constine, Josh. "Facebook Acquires Assets Of UK Mobile Bug-Checking Software Developer Monoidics | TechCrunch". Techcrunch.
  6. Finley, Klint. "Facebook's AI Tool for Squashing Bugs Is Now Open to All | WIRED". www.wired.com.
  7. O'Sullivan, Bryan. "Four Facebook Employees Win the Prestigious CAV Award". Facebook Research.
  8. Separation logic and bi-abduction, page, Infer project site.
  9. Calcagno, Cristiano; Distefano, Dino; Dubreil, Jeremy; Gabi, Dominik; Hooimeijer, Pieter; Luca, Martino; O’Hearn, Peter; Papakonstantinou, Irene; Purbrick, Jim; Rodriguez, Dulma (27 April 2015). Moving Fast with Software Verification. NASA Formal Methods. Lecture Notes in Computer Science. 9058. Springer, Cham. pp. 3–11. doi:10.1007/978-3-319-17524-9_1. ISBN 978-3-319-17523-2.
  10. Churchill, Dulma; Distefano, Dino; Luca, Martino; Rhee, Ryan; Villard, Jules. "AL: A new declarative language for detecting bugs with Infer". Facebook Code Blog Post.
  11. Sergio, de Simone. "Facebook's New AL Language Aims to Simplify Static Program Analysis". InfoQ.
  12. "Infer Github Page".
  13. "Silver Medals for UK's brightest up-and-coming tech entrepreneurs". Royal Academy of Engineering. Archived from the original on 2014-10-26. Retrieved 2017-07-05.
  14. committee, CAV Award. "2016 Computer-Aided Verification Award". PRLog.
  15. "RAEng New Fellows 2016, Peter O'Hearn". Royal Academy of Engineering.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.