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

Material type: 文書・図像類

Author: 寺内, 多智弘

Publisher: -

Publication date: 2017-05-31

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: 本課題の目標は、関数型プログラミング言語など、高階関数を含むプログラミング言語で記述された大規模ソフトウェアに対して有効な自動検証手法の確立である。特に、近年、国内外において高く注目されている依存型型システムを用いたソフトウェアモデル検査による手法を研究した。主な研究成果は以下である：1.)よりよい...

Search by Bookstore

Holdings of Libraries in Japan

This page shows libraries in Japan other than the National Diet Library that hold the material.

List of Cooperating Institutions and Databases

Please contact your local library for information on how to use materials or whether it is possible to request materials from the holding libraries.

other

JAIST Repository
Digital
You can check the holdings of institutions and databases with which 学術機関リポジトリデータベース（IRDB）（機関リポジトリ） is linked at the site of 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）.
JAIST Repository

Search by Bookstore

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

Material Type: 文書・図像類
Title: 高階プログラミング言語で記述された大規模ソフトウェアの検証
Author/Editor: 寺内, 多智弘
Author Heading: 寺内, 多智弘
Publication Date: 2017-05-31
Publication Date (W3CDTF): 2017-05-31
Alternative Title: Large scale verification of higher-order programs
Periodical title: 科学研究費助成事業研究成果報告書
Pages: 1-4
Text Language Code: jpn
Subject Heading: プログラム検証
モデル検査
高階関数
述語論理
型システム
抽象詳細化
時相論理
Target Audience: 一般
Note (General): 本課題の目標は、関数型プログラミング言語など、高階関数を含むプログラミング言語で記述された大規模ソフトウェアに対して有効な自動検証手法の確立である。特に、近年、国内外において高く注目されている依存型型システムを用いたソフトウェアモデル検査による手法を研究した。主な研究成果は以下である：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
Format (IMT): application/pdf
Source: https://dspace.jaist.ac.jp/dspace/bitstream/10119/14316/1/26330082seika.pdf
https://dspace.jaist.ac.jp/dspace/bitstream/10119/14316/1/26330082seika.pdf
Access Restrictions: 限定公開
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ