プログラム解析についての現場視点

記事

• 実際の使用経験に基づく、形式的プログラム解析への実践者からの批評
• 形式的証明と非形式的な現実のギャップが核心的な弱点だと主張
• 解析ツールが実際に何を提供するか、その理論的な約束との乖離に焦点

ディスカッション

• あるコメント投稿者は、形式/非形式のギャップへの批判は1979年の論文に遡ると指摘
• 別の投稿者は、著者がSAT/SMTソルバー（制約充足問題を解くための自動定理証明ツール）のエコシステムを全く認識していないようだと述べる

HNで議論を見る

原文（英語）: My practitioner view of program analysis