Logic

プログラムを1回も動かさずに、なぜ「絶対にバグが起きない」と証明できるのか：形式検証とモデル検査の科学