|
JAIST Repository >
b. 情報科学研究科・情報科学系 >
b50. 科学研究費助成事業研究成果報告書 >
2016年度 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/14316
|
| タイトル: | 高階プログラミング言語で記述された大規模ソフトウェアの検証 |
| その他のタイトル: | Large scale verification of higher-order programs |
| 著者: | 寺内, 多智弘 |
| 著者（別表記）: | Terauchi, Tachio |
| キーワード: | プログラム検証
モデル検査
高階関数
述語論理
型システム
抽象詳細化
時相論理 |
| 発行日: | 31-May-2017 |
| 抄録: | 本課題の目標は、関数型プログラミング言語など、高階関数を含むプログラミング言語で記述された大規模ソフトウェアに対して有効な自動検証手法の確立である。特に、近年、国内外において高く注目されている依存型型システムを用いたソフトウェアモデル検査による手法を研究した。主な研究成果は以下である：1.)よりよい抽象詳細化(ソフトウェアモデル検査に用いられる技術)の手法、2.)高階関数型プログラムのための停止性・活性仕様など時相論理仕様の自動検証手法。：The goal of the research is to advance the state of the art on automatic verification techniques of higher-order functional programs. We have especially focused on the techniques based on software model checking via dependent type inference, that has gained popularity in the recent years. The main contributions of the research are as follows: 1.) New, improved abstraction refinement methods (abstraction refinement is a technique used in software model checking), 2.) New automatic methods for verification of temporal properties (such as termination and liveness) of higher-order functional programs. |
| 記述: | 基盤研究(C)（一般）
研究期間：2014～2016
課題番号：26330082
研究者番号：70447150
研究分野：ソフトウェア |
| 言語: | jpn |
| URI: | http://hdl.handle.net/10119/14316 |
| 出現コレクション: | 2016年度 (FY 2016)
|
このアイテムのファイル:
| ファイル |
記述 |
サイズ | 形式 |
|---|
| 26330082seika.pdf | | 86Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|
