仮想的なタグを用いた共用体入りプログラムの事前条件推定

今井 健男, 酒井 政裕, 遠藤 侑介, 萩谷 昌己 「仮想的なタグを用いた共用体入りプログラムの事前条件推定」, 第14回プログラミングおよびプログラミング言語ワークショップ (PPL2012), p. 146 (ポスター), 2012年3月.

概要 / Abstract

本発表では、共用体を用いた C 言語プログラムの検証方法を提案する。本手法では、共用体変数が直和型を持つと読み替える。具体的には、代入時、代入されたフィールドと同じ型タグを付加的に記憶し、また、タグと異なるフィールドからの読み出しで例外を発生するようにプログラムを読み替える。その上で、我々の先行研究に基づき、プログラムテキストから生成した述語の組み合わせで最も弱い事前条件(準最弱事前条件)を有界モデル検査器を使って求めることで、共用体を用いたプログラムが安全に利用される条件を推定する。我々は本手法をツールに試作し、予備的な評価を行った。