氏名: 大原 直美 (089730380)

論文題目: 定理自動証明システム Isabelle を用いたプログラム検証の自動化


論文概要

プログラムが期待された結果を出すことを証明することができれば、 作成されたプログラムの正当性を保証することができる。 プログラムの検証法の一つとして、前条件と後条件を持つ プログラムに推論規則を適用していくことでプログラムの正当性を 検証するものがある。

本研究では、プログラムの正当性証明を 汎用な定理自動証明システム Isabelle の上で自動化する。 具体的には、対象のプログラミング言語を Isabelle 上でデータ構造化し、 それに基づいて各推論規則を宣言して、theoryを構成する。 作成されたtheoryに基づき証明手順をIsabelleに指示することにより 証明は自動的に実行される。


目次に戻る


提出時刻:2001/02/08 17:22:01