定理証明器によって証明されたCプログラムのマージャ

後藤, 裕貴, 高橋, 和子

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

The purpose of this study is to propose a manner of a usage of a theorem prover in software verification process and to expand an application area of theorem proving. As a case study, we construct a certified merger for C programs, which is verified using a theorem prover Isabelle/HOL. It is a merge system that generates a merged code with some optimization of a given pair of C programs. Our target is a subset of a real C language. The main part of the system is both written and proved by Isabelle/HOL. The front-end part and the back-end part are implemented in C. It provides a useful tool for users who are not familiar with theorem provers. We prove several lemmas on syntactical correctness. For example, the merged program includes no duplication of variable names, and there exist the corresponding renamed definitions of functions. Mergers are used for a test program of test suits in the process of software verification or in a distributed environment for software development. The certified merger can improve the reliability of these processes. In addition, if we provide our proof as a library of Isabelle/HOL, more usage of theorem provers is promising.

定理証明器によって証明されたCプログラムのマージャ

書誌事項

この論文をさがす

抄録

収録刊行物

キーワード

詳細情報詳細情報について

書き出し

問題の指摘

定理証明器によって証明されたCプログラムのマージャ

書誌事項

この論文をさがす

抄録

収録刊行物

キーワード

詳細情報 詳細情報について

書き出し

問題の指摘

参加プロジェクトリスト

詳細情報詳細情報について