추론 정적 분석기

Infer Static Analyzer

"[1]Facebook User"로 불리기도 하는 Expend는 Facebook의 엔지니어링 팀이 오픈 소스 기여자들과 함께 개발한 정적 코드 분석 도구입니다.Java, C, C++, Objective-C를 지원하며, Android 및 iOS 앱(WhatsApp, Instagram, Messenger 및 주요 Facebook [2]앱 포함) 분석에 Facebook에서 배포됩니다.

역사

인듀어는 소프트웨어의 공식 검증을 위한 이론인 분리 논리에 대한 학술 연구에 뿌리를 두고 있습니다.Separation Logic에 기반한 자동 프로그램 검증 작업은 Smallfoot 및 SpaceInvader 등의 일련의 학술 도구로 이어졌습니다.이 학술적인 연구를 바탕으로 2009년 런던에 있는 3명의 연구자 크리스티아누 칼사그노, 디노 디스테파노, 피터 오헌이 검증 스타트업 모노이딕스를 공동 설립했으며 모노이딕스는 [3][4][2]인듀어의 첫 버전을 개발했다.Monoidics는 [5]2013년에 Facebook에 인수되었고, 2015년에는 User의 코드가 오픈 [2][6]소스되었다.

2013년, 인듀어가 오픈 소스 되었을 때, 인듀어가 식별한 월 수백 개의 버그가 Facebook의 개발자에 의해서 [5]실전에 도달하기 전에 수정되었다고 주장되고 있다.2015년에는 [7]월 1000개 이상의 버그로 증가했습니다.

Spotify, Uber, Mozilla, Sky 및 Marks and Spencer가 보고된 사용자 [1]중 하나입니다.

테크놀로지

Include는 Android 및 Java 코드에서 늘 포인터의 예외, 리소스 누수, 주석 도달 가능성, 잠금 가드 누락 및 동시성 경쟁 조건을 확인합니다.C, C++ 및 Objective [1]C에서 늘 포인터의 문제, 메모리 누수, 코딩 규칙 및 사용할 수 없는 API를 확인합니다.

인추어는 바이 압추라고[8] 불리는 기술을 사용하여 프로그램 프로시저를 호출자와 독립적으로 해석하는 구성 프로그램 분석을 수행합니다.이를 통해 대규모 코드베이스를 확장하고 증분 방식으로 코드 변경에 대해 신속하게 실행할 수 있는 동시에 절차 [9]경계를 넘어 추론하는 프로시저 간 분석을 수행할 수 있다고 주장합니다.

인투어는 페이스북의 코드 리뷰 시스템에 연결되어 있다.코드 수정에 대한 코멘트는 코드 수정이 검토용으로 제출될 때 자동으로 코멘트를 제공하는 배치 모델로, 코드 수정은 잠재적인 퇴행을 보고합니다.데이터 [9]센터에서 실행되는 Facebook의 지속적인 통합 시스템 상의 작업을 통해 코드 변경을 점진적으로 분석함으로써 이를 실현합니다.

또한 계산 트리 [10]로직을 위한 모델 확인의 아이디어를 기반으로 추상 구문 트리 보풀을 위한 도메인별 언어도 있습니다.[11]

추론은 주로 OCaml 프로그래밍 [12]언어로 작성됩니다.

어워드

디노 디스테파노는 [it] 모노이딕스 [13]인수를 인정받아 2014년 왕립공학아카데미 은메달을 수상했다.

Josh Berdine, Cristiano Calcagno, Dino Distafano, Peter O'Hearn 등 4명의 Uppor 팀이 John C와 공동으로 2016 Computer Aided Verification Award를 수상했습니다. 레이놀즈, 삼인 이스티아크,[7][14] 양홍석.

Peter O'Hearn은 분리논리와 [15]추론 연구로 2016년에 왕립공학아카데미의 펠로우로 선출되었다.

레퍼런스

  1. ^ a b c "Infer static analyzer". Website.
  2. ^ a b c 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. Vol. 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. ^ a b 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. ^ a b O'Sullivan, Bryan. "Four Facebook Employees Win the Prestigious CAV Award". Facebook Research.
  8. ^ 분리논리와 이연산, 페이지, 프로젝트 현장 추론.
  9. ^ a b 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. Vol. 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.

외부 링크