抽象解釈は博士学位が必要に聞こえる。もうそうではない
Inferを使ってCIパイプラインで形式的静的解析を実行する方法。動作する設定と現実的なトレードオフを紹介する。
抽象解釈は、エンジニアがタブを閉じてしまうような言葉だ。束理論を一学期学ばなければ理解できないようなものに聞こえる。ほとんどの開発者は、それが研究論文の世界のもので、プルリクエストの世界のものではないと思い込んでいる。…
2 posts
Inferを使ってCIパイプラインで形式的静的解析を実行する方法。動作する設定と現実的なトレードオフを紹介する。
抽象解釈は、エンジニアがタブを閉じてしまうような言葉だ。束理論を一学期学ばなければ理解できないようなものに聞こえる。ほとんどの開発者は、それが研究論文の世界のもので、プルリクエストの世界のものではないと思い込んでいる。…
MetaのInferは抽象解釈と双方向誘導を用いて、コードの構造を推論することでヌル参照、メモリリーク、競合状態を検出する。実行は不要だ。仕組みと自社コードベースでの活用方法を解説する。
Metaは、コードがユーザーに到達する前に静的解析ツールが捉えた10万件以上のバグ修正をリリースしてきた。そのツールはInferと呼ばれ、オープンソースであり、コードを実行しない。コードを読み込み、コードが可能な動作の数学モデルを構築し、特定の有害な事象が起こりえないことを証明する。あるいは、それが起こりうる経路を発見…