Loading article…
Infer [1]は、「Facebook Infer」とも呼ばれ、Facebook のエンジニアリングチームとオープンソースの貢献者によって開発された静的コード解析ツールです。Java 、C、C++、Objective-Cをサポートしており、FacebookのAndroidおよびiOSアプリ（WhatsApp、Instagram、Messenger、メインのFacebookアプリを含む）の解析に使用されています。[2]
歴史
Infer は、ソフトウェアの形式検証理論である分離論理に関する学術研究に端を発しています。分離論理に基づく自動プログラム検証の研究は、Smallfoot や SpaceInvader などの一連の学術ツールにつながりました。この学術研究を基に、ロンドン大学ユニバーシティ・カレッジとロンドン大学クイーン・メアリー校の 3 人の研究者であるCristiano Calcagno、Dino Distefano、 Peter O'Hearn は、2009 年に検証スタートアップ企業 Monoidics を共同設立し、Monoidics が Infer の最初のバージョンを開発しました。[3] [4] [2] Monoidics は 2013 年に Facebook に買収され、[5] 2015 年に Infer のコードがオープンソース化されました。[2] [6]
Inferがオープンソース化された2013年の時点では、Inferによって特定された毎月数百のバグが、実稼働環境に到達する前にFacebookの開発者によって修正されたと主張されていました。[5] 2015年までに、これは毎月1000を超えるバグに増加しました。[7]
Inferのユーザーとして報告されている企業には、Spotify、Uber、Mozilla、Sky、Marks and Spencerなどがある。[1]
テクノロジー
Inferは、AndroidおよびJavaコードにおけるヌルポインタ例外、リソースリーク、アノテーション到達可能性、ロックガードの欠落、同時実行競合状態のチェックを実行します。C、C++、Objective Cにおけるヌルポインタ問題、メモリリーク、コーディング規約、利用できないAPIをチェックします。[1]
Inferは、バイアブダクション[8]と呼ばれる手法を使用して、呼び出し元から独立してプログラムプロシージャを解釈する構成プログラム解析を実行します。これにより、Inferは大規模なコードベースに拡張でき、コード変更を増分的に迅速に実行しながら、プロシージャの境界を越えて推論するプロシージャ間解析を実行できると言われています。[9]
Infer は Facebook のコードレビュー システムに接続されています。その展開モデルは、レビューのために提出されたコード変更に自動的にコメントを付け、潜在的な回帰を報告するというものです。これは、Facebook のデータセンターで実行される継続的インテグレーションシステムのジョブを介してコード変更を段階的に分析することによって行われます。[9]
Inferには、計算木ロジックのモデル検査のアイデアに基づいた抽象構文木リンティング用のドメイン固有言語もあります。[10] [11]
Inferは主にOCamlプログラミング言語で書かれています。[12]
受賞歴
ディノ・ディステファーノ [it]は、モノイディクスの買収が認められ、2014年に王立工学アカデミーの銀メダルを受賞しました。 [13]
Inferチームメンバーの4人、ジョシュ・バーディン、クリスティアーノ・カルカニョ、ディノ・ディスタファノ、ピーター・オハーンは2016年のコンピュータ支援検証賞を受賞し、ジョン・C・レイノルズ、サミン・イシュティアク、ホンソク・ヤンと共同受賞した。[7] [14]
ピーター・オハーンは、分離論理とInferに関する研究により、2016年に王立工学アカデミーのフェローに選出されました。 [15]
参考文献
- ^ abc 「Infer 静的アナライザー」。ウェブサイト。
- ^ abc Calcagno, Cristiano; Distefano, Dino; O'Hearn, Peter. 「Facebook Infer のオープンソース化: 出荷前にバグを特定する」。
- ^ Calcagno, Cristiano; Distefano, Dino; O?Hearn, Peter W.; Yang, Hongseok (2011年12月1日). 「Bi-Abductionによる構成形状分析」Journal of the ACM . 58 (6): 1–66. CiteSeerX 10.1.1.420.2150 . doi :10.1145/2049697.2049700.
- ^ Calcagno, Cristiano; Distefano, Dino (2011 年 4 月 18 日)。「Infer: C プログラムのメモリ安全性のための自動プログラム検証ツール」。NASA形式手法。コンピュータ サイエンスの講義ノート。第 6617 巻。Springer、ベルリン、ハイデルベルク。pp. 459–465。CiteSeerX 10.1.1.421.9629。doi : 10.1007 / 978-3-642-20398-5_33。ISBN 978-3-642-20397-8。
- ^ ab Constine, Josh. 「Facebook が英国のモバイル バグ チェック ソフトウェア開発会社 Monoidics の資産を買収 | TechCrunch」。Techcrunch。
- ^ Finley, Klint. 「Facebook のバグ撲滅 AI ツールが一般公開 | WIRED」www.wired.com。
- ^ ab オサリバン、ブライアン。「Facebook の従業員 4 名が名誉ある CAV 賞を受賞」。Facebook リサーチ。
- ^ 分離論理とバイアブダクション、ページ、Infer プロジェクト サイト。
- ^ ab Calcagno, Cristiano; Distefano, Dino; Dubreil, Jeremy; Gabi, Dominik; Hooimeijer, Pieter; Luca, Martino; O'Hearn, Peter; Papakonstantinou, Irene; Purbrick, Jim; Rodriguez, Dulma (2015 年 4 月 27 日)。「ソフトウェア検証による迅速な移行」NASA形式手法。コンピュータ サイエンスの講義ノート。第 9058 巻。Springer、Cham。pp. 3–11。doi : 10.1007/978-3-319-17524-9_1。ISBN 978-3-319-17523-2。
- ^ Churchill, Dulma; Distefano, Dino; Luca, Martino; Rhee, Ryan; Villard, Jules. 「AL: Infer でバグを検出するための新しい宣言型言語」。Facebook Code ブログ投稿。
- ^ Sergio, de Simone. 「Facebook の新しい AL 言語は静的プログラム分析の簡素化を目指しています」。InfoQ。
- ^ 「 Githubページを推測する」。GitHub 。
- ^ 「英国で最も優秀な新進気鋭の技術系起業家に銀メダル」。王立工学アカデミー。2014年10月26日時点のオリジナルよりアーカイブ。2017年7月5日閲覧。
- ^ 委員会、CAV 賞。「2016 コンピュータ支援検証賞」。PRLog。
- ^ 「RAEng New Fellows 2016、Peter O'Hearn」。王立工学アカデミー。
外部リンク
- 公式サイト