私は正式な検証について読んでいますが、基本的なポイントは、正式な仕様とモデルを使用する必要があるということです。ただし、多くの情報源は静的解析を正式な検証手法として分類しており、一部は抽象的な解釈に言及し、コンパイラでの使用に言及しています。だから私は混乱しています-モデルの正式な説明がない場合、これらはどのように正式な検証になるのでしょうか?
編集：私が見つけたソースは次のとおりです：
静的分析: 定義済みの抽象化に従って、プログラム テキストから抽象セマンティクスが自動的に計算されます (ユーザーが自動/手動で調整できる場合もあります)。
では、正式な仕様を必要とせずにソース コードだけで動作するということですか? これは、静的アナライザーが行うことです。
また、正式な検証なしで静的解析は可能ですか? たとえば、SonarQube は本当に正式なメソッドを実行しますか?
静的分析とは、「ソースコードを読んで、おそらく文句を言う」ことを意味します。（「動的分析」とは対照的に、「プログラムを実行し、実行動作について不平を言う可能性がある」ことを意味します）。
考えられる静的分析の苦情には、さまざまな種類があります。考えられる苦情の1つは、
Your source code does not provably satisfy a formal specification
この苦情は、静的アナライザーが「形式的に」解釈する形式的な仕様、ソース コードの形式的な解釈、および適切な定理を見つけることができなかった信頼できる定理証明者を持っている場合、形式的な検証に基づいています。
静的アナライザーから得られる可能性のある他の種類の苦情はすべて、ヒューリスティックな意見です。つまり、コード (または、実際に存在する場合は仕様) の非公式な解釈に基づいています。
Coverity などの「ヘビー デューティー」な静的アナライザーにはかなり優れたプログラム モデルがありますが、コードが仕様を満たしているかどうかはわかりません (仕様があるかどうかを確認することさえしません)。せいぜい、コードが言語に応じて未定義のことを行うこと（「ヌルポインターの逆参照」）を伝えるだけであり、その苦情でさえ常に正しいとは限りません。
MISRA などのいわゆる「スタイル チェッカー」も静的アナライザーですが、彼らの不満は基本的に「一部の委員会が不適切な形式であると判断した構造を使用した」というものです。それは実際にはバグではなく、純粋な意見です。