定理証明器によって証明されたCプログラムのマージャ
スポンサーリンク
概要
- 論文の詳細を見る
本研究の目的は,ソフトウェア検証過程における定理証明の利用方法の提案と,定理証明の応用領域の拡張である.我々は,ケーススタディとして定理証明器Isabelle/HOLでシステム仕様を保証したCプログラムマージャを構築する.これは,与えられた2つのCプログラムのソースコードに対し,それらを併合し,いくつかの最適化を施したCプログラムソースコードを出力するマージシステムである.また,ここで扱うCプログラムは実際のC言語の部分集合である.本システムの主要部分はIsabelle/HOLで記述し証明しており,フロントエンドとバックエンドはCプログラムで実装している.本システムは,フロントエンドとバックエンドを備えることで,定理証明器に不慣れなユーザにも使いやすいツールとして提供可能である.証明では,マージ後のプログラムが変数名の重複を含まないこと,改名された関数定義が必ず存在することなど,構文的な正当性のみを対象とした.マージャはソフトウェアテストにおけるテストスイートや,分散開発環境でのプログラムソースの併合などで用いられ,仕様を証明したものを提供することで,これを使って開発されたシステムの信頼性が向上する.また,このマージャをIsabelle/HOLのライブラリとして提供することで,定理証明の応用事例の増加も期待できる.
- 2013-08-29
著者
関連論文
- 知識変更を伴う議論システム
- 鉄道信号システムの連動装置の形式的検証向けモデル化と検証環境構築(ソフトウェア基礎, プログラム理論)
- 車車間通信を用いた車線変更と脇道にともなう交通流の円滑化を図るモデルの提案と実装
- 帰納的アプローチに基づく理想的電子現金方式のモデル化および証明支援系Isabelle/HOLによる安全性の証明
- 電子現金の分割利用可能性の形式化と帰納的証明
- 車車間通信を用いた車線変更と脇道にともなう交通流の円滑化を図るモデルの提案と実装
- Symmetry Reductionを使ったAISの確率付きモデル検査
- 定性空間推論の新しい枠組DLCSとその上での操作
- 矩形領域に基づく定性空間推論の提案と実装
- 凹凸情報と接触パターンに基づく定性空間表現
- 定理証明器による電子現金プロトコルの検証
- 信念改竄によるばれない嘘の生成
- 輻輳問題を考慮したモバイルエージェントによるアドホックネットワークルーティング(モバイル・アドホックネットワーク(1))
- 定性空間表現の二次元平面への埋め込みについて
- 定性空間表現の二次元平面への埋め込みについて
- ボードゲームBAOにおける周期的動作の解析
- ボードゲームBAOにおける周期的動作の解析(数理モデル一般)
- ボードゲームBAOのCCSによる記述と解析
- 性質の伝播に関する定性空間推論
- モバイルエージェントを用いた動的ネットワークルーチングシステムの拡張
- 空間に埋め込まれた意味情報の記述
- マルチエージェントの連鎖的交渉を用いたスケジュール作成と調整(スケジューリング,「Webインテリジェンス」及び一般)
- マルチエージェントの連鎖的交渉を用いたスケジュール作成と調整(スケジューリング,「Webインテリジェンス」及び一般)
- 動的議論システムの意味論的考察
- 「情報処理学会論文誌 : プログラミング」の編集について
- 「情報処理学会論文誌 : プログラミング」の編集について
- 矩形同士の埋め込み型重ね合わせについての定性空間推論
- 定理証明器によって証明されたCプログラムのマージャ