情報処理学会 第75回全国大会講演要旨

モデル検査はプログラムから不具合を網羅的に探索し、発見すれば不具合に至る実行経路を反例として出力させることができる。しかし、反例だけを見てプログラムの具体的な修正方法を考えるのが困難なときがある。そこでモデル検査で出力させた反例から修正方法を提示するツールを開発した。具体的には反例情報をもとに実行順序の逆をたどることで、不具合の原因となる処理を特定し、それに基づいて修正案を提示する。本ツールはC言語を対象としており、モデル検査ツールCBMCを用いた。検出する不具合は、フリーズなどの原因となる反例やポインタによるメモリ範囲外参照を対象としている。