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

• Item type: Trans(1)
• 公開日: 2013-08-29
• タイトル: 定理証明器によって証明されたCプログラムのマージャ
• タイトル / 言語: en
• タイトル: Certified Merger for C Programs Using a Theorem Prover
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 関西学院大学理工学部情報科学科
• 著者所属: 関西学院大学理工学部情報科学科
• 著者所属(英): en
• 著者所属(英): School of Science and Technology, Kwansei Gakuin University
• 著者所属(英): en
• 著者所属(英): School of Science and Technology, Kwansei Gakuin University
• 著者名: 後藤, 裕貴; 高橋, 和子
• 著者名(英): Yuki, Goto; Kazuko, Takahashi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本研究の目的は，ソフトウェア検証過程における定理証明の利用方法の提案と，定理証明の応用領域の拡張である．我々は，ケーススタディとして定理証明器Isabelle/HOLでシステム仕様を保証したCプログラムマージャを構築する．これは，与えられた2つのCプログラムのソースコードに対し，それらを併合し，いくつかの最適化を施したCプログラムソースコードを出力するマージシステムである．また，ここで扱うCプログラムは実際のC言語の部分集合である．本システムの主要部分はIsabelle/HOLで記述し証明しており，フロントエンドとバックエンドはCプログラムで実装している．本システムは，フロントエンドとバックエンドを備えることで，定理証明器に不慣れなユーザにも使いやすいツールとして提供可能である．証明では，マージ後のプログラムが変数名の重複を含まないこと，改名された関数定義が必ず存在することなど，構文的な正当性のみを対象とした．マージャはソフトウェアテストにおけるテストスイートや，分散開発環境でのプログラムソースの併合などで用いられ，仕様を証明したものを提供することで，これを使って開発されたシステムの信頼性が向上する．また，このマージャをIsabelle/HOLのライブラリとして提供することで，定理証明の応用事例の増加も期待できる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 6, 号 2, p. 103-103, 発行日 2013-08-29
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会