CForge: C言語プログラムのための有界検査ツール

酒井政裕, 今井健男,「CForge: C言語プログラムのための有界検査ツール」, 第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009), pp. 118-132, 2009年3月.

Abstract

Forge は Dennis らによって開発されているプログラム検査エンジンであり、ヒープ操作を含むようなプログラム及び仕様を関係論理と呼ばれる論理で表現し、プログラムが仕様を満たしているかを SAT ソルバを用いた有界モデル検査 (Bounded Model Checking) によって検査することが出来る。しかし、Forge は Javeに適用することを念頭に作られているため、C 言語のようなポインタ演算を持つ言語へはそのまま適用できない。我々は Forge を用いて C 言語プログラムの検査を行うツール CForge の開発を試みた。本稿ではその実装方法と評価について述べる。

我々は、C 言語特有のポインタ演算を関係論理で表現するために Fat Pointer に基づいた方法を用い、仕様記述言語としては JML 風の言語を用いた。また、CForge を用いて C 言語の標準ライブラリの一部や初等的なアルゴリズムの検証を行った。

Links: