概要
　本研究の目的は，ソフトウェア検証過程における定理証明の利用方法の提案
と，定理証明の応用領域の拡張である．我々は，ケーススタディとして定理証
明器 Isabelle/HOL でシステム仕様を保証した C プログラム併合システムを構
築する．これは，与えられた 2 つの C プログラムのソースコードに対し，そ
れらを併合し，いくつかの最適化を施した C プログラムソースコードを出力す
る併合システムである．また，ここで扱う C プログラムは実際の C 言語の部
分集合である．本システムの主要部分はIsabelle/HOL で記述し証明しており，
フロントエンドとバックエンドは C プログラムで実装している．本システムは，
フロントエンドとバックエンドを備えることで，定理証明器に不慣れなユーザ
にも使いやすいツールとして提供可能である．併合については，併合後のプロ
グラムが変数名の重複を含まないこと，改名された関数定義が必ず存在するこ
となど，構文的な正当性のみを対象として形式化し，証明を完了した．最適化
については，形式化は行ったが証明は完了していない．併合システムはソフト
ウェアテストにおけるテストスイートや，分散開発環境でのプログラムソース
の併合などで用いられ，仕様を証明したものを提供することで，これを使って
開発されたシステムの信頼性が向上する．また，この併合システムを 本研究の
成果により，Isabelle/HOL のライブラリとして提供することで，定理証明の応
用事例の増加も期待できる．

発表論文
 
``定理証明器によって証明された C プログラムのマージャー,''
情報処理学会第92回プログラミング研究会発表資料, January, 2013.

``Certified Merger for C Programs Using
a Theorem Prover:A First Step,'' 
28th International Conference on Computers and Their Applications (CATA2013),
pp.59-64, March, 2013.