形式的検証 - entropy

形式的検証

format varification

ソフトウェアが正しく動作することを数学的に証明する手法

論理的・数学的なモデルを用いて正しいことを検証する

具体的には、プログラムが特定の仕様（要件）を満たしていることを、手動またはツールを用いて証明する

テストとは、形式的検証ではロジックを解析して正しさを確認する点で異なる

具体的なツール

Prusti: コードを静的解析して形式的検証を行うツール

KLEE: コードをシンボリック実行で解析し、検証を支援するツール