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

@inproceedings{citeulike:4275278, abstract = {ForgeはDennisらによって開発されているプログラム検査エンジンであり、ヒープ操作を含むようなプログラム及び仕様を関係論理と呼ばれる論理で表現し、プログラムが仕様を満たしているかをSAT ソルバを用いた有界モデル検査(Bounded Model Checking)によって検査することが出来る。しかし、ForgeはJaveに適用することを念頭に作られているため、C言語のようなポインタ演算を持つ言語へはそのまま適用できない。我々はForge を用いてC言語プログラムの検査を行うツールCForgeの開発を試みた。本稿ではその実装方法と評価について述べる。 我々は、C 言語特有のポインタ演算を関係論理で表現するためにFat Pointer に基づいた方法を用い、仕様記述言語としてはJML 風の言語を用いた。また、CForge を用いてC 言語の標準ライブラリの一部や初等的なアルゴリズムの検証を行った。}, author = {Sakai, Masahiro and Imai, Takeo}, citeulike-article-id = {4275278}, keywords = {alloy, ppl2009}, posted-at = {2009-04-05 08:12:44}, priority = {0}, title = {CForge: C言語プログラムのための有界検査ツール} }

TY - CONF ID - citeulike:4275278 L3 - citeulike-article-id:4275278 N2 - ForgeはDennisらによって開発されているプログラム検査エンジンであり、ヒープ操作を含むようなプログラム及び仕様を関係論理と呼ばれる論理で表現し、プログラムが仕様を満たしているかをSAT ソルバを用いた有界モデル検査(Bounded Model Checking)によって検査することが出来る。しかし、ForgeはJaveに適用することを念頭に作られているため、C言語のようなポインタ演算を持つ言語へはそのまま適用できない。我々はForge を用いてC言語プログラムの検査を行うツールCForgeの開発を試みた。本稿ではその実装方法と評価について述べる。 我々は、C 言語特有のポインタ演算を関係論理で表現するためにFat Pointer に基づいた方法を用い、仕様記述言語としてはJML 風の言語を用いた。また、CForge を用いてC 言語の標準ライブラリの一部や初等的なアルゴリズムの検証を行った。 TI - CForge: C言語プログラムのための有界検査ツール KW - alloy KW - ppl2009 AU - Sakai, Masahiro AU - Imai, Takeo ER -