形式検証ツールAlive2の「見逃しアラーム」バグを探る

Looking for Missed Alarm Bugs in a Formal Verification Tool

形式検証は魔法ではなく、Alive2のようなツール自体にもバグが潜む。Alive2はLLVMの最適化を検証する翻訳検証ツールで、誤ったアラーム（false alarm）と見逃しアラーム（missed alarm）の2種類の欠陥があり得る。後者の発見は難しく、著者らはYARPGenを改造したランダム差分テストと、Minotaurスーパーオプティマイザーを利用した2つの手法を試した。結果、現時点ではAlive2は見逃しバグを起こしていないが、関数属性など未検証の領域が残る。