--- tags: 論文メモ --- # Modelling Program Verification Tools for Software Engineers ## 背景 ### 問題意識 - プログラム検証によってエンドユーザーが問題を解決しようとするとき,情報収集が難しい - プログラム検証ツールのどれをどんな問題に適用すればいいか判断するには高度な知識と相当期間の情報収集が必要になってくる - 論文書いてメンテ終了などよくあり,プロトタイプで終わってるとか - リポジトリにドキュメントが一切なくて論文読めとか ### 問題への貢献 - プログラム検証ツールの分類 - PV0-6 - 読みやすいまとめ<https://slebok.github.io/proverb> ## 具体的な手法など - プログラム検証関連のツールを7つに分類(直感的にはレベルが高いほど保証が強い) - 証明の役割分担 - claim: 証明したい性質に関する主張 - verifier: argumentを何らかの方法で精査してpass/fail とできる - prover: claimを証明するための操作・計算をしてargumentを生成する - argument - モデル - mapping property: 現実の一部を反映 - reduction property: 現実の事象の最も重要と思われる部分以外を捨象している - pragmatic property: 目的を持ってモデル化されている - 形式モデル: モデルの具体例で数学的な形式化がなされたもの - PV0: 形式モデルが存在するが正確性の保証に貢献しない - PV1: proverが存在しない. verifierであるようなツール. 形式モデルの性質を自動的に検査 - PV2: ユーザーの記述をモデルとして実装を生成する. 生成された実装をさらに違うツールに噛ませるとよりたかいPVになる - PV3: ユーザーによる明示的な性質への要求が与えられ,それを実装が満たすか検証できる - PV4: ユーザーが明示的に指定した性質以外のものも導出できる - 未定義動作無し→諸々の条件みたいな変換ができるようなやつ - 部分的な無視もできる - PV5: どの性質を検証するか・どのように推論するかを指定できる(specification compiler) - PV4のツールはPV5のフレームワーク上に実装されることもある - PV6: 異なる仕様を扱えるだけでなく証明の正しさまで保証できる(proof assistant)