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

寺内, 多智弘

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

https://dspace.jaist.ac.jp/dspace/bitstream/10119/14316/1/26330082seika.pdf

Number of accesses :  

Other information