高階プログラミング言語で記述された大規模ソフトウェアの検証

• 資料種別: 文書・図像類
• タイトル: 高階プログラミング言語で記述された大規模ソフトウェアの検証
• 著者・編者: 寺内, 多智弘
• 著者標目: 寺内, 多智弘
• 出版年月日等: 2017-05-31
• 出版年（W3CDTF）: 2017-05-31
• 並列タイトル等: Large scale verification of higher-order programs
• タイトル（掲載誌）: 科学研究費助成事業研究成果報告書
• 掲載ページ: 1-4
• 本文の言語コード: jpn
• 件名標目: プログラム検証; モデル検査; 高階関数; 述語論理; 型システム; 抽象詳細化; 時相論理
• 対象利用者: 一般
• 一般注記: 本課題の目標は、関数型プログラミング言語など、高階関数を含むプログラミング言語で記述された大規模ソフトウェアに対して有効な自動検証手法の確立である。特に、近年、国内外において高く注目されている依存型型システムを用いたソフトウェアモデル検査による手法を研究した。主な研究成果は以下である：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; 研究分野：ソフトウェア; identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/14316
• 記録形式（IMT）: application/pdf
• 一次資料へのリンクURL: https://dspace.jaist.ac.jp/dspace/bitstream/10119/14316/1/26330082seika.pdf
• オンライン閲覧公開範囲: 限定公開
• 連携機関・データベース: 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• 提供元機関・データベース: 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ