並列タイトル等Automating program verification on the data management domain
一般注記本研究では、データ管理領域に焦点を当て、プログラム検証を自動化する手法を提案した。データ管理システムに特有の繰り返し処理を行う命令、推論規則を導入した言語を定義し、検証条件自動生成器を実装した。推論規則をループ不変表明に依存しないものとすることにより、検証条件の自動生成を可能とした。今後、検証条件の生成効率の改善、言語の表現力の拡張に関して検討する必要がある。 : In this research, we proposed a method to automate the program verification for the systems in the data management domain. We defined a language which has loop statements and inference rules tailored for the domain and implemented a verification condition generator. We made it possible to automatically generate verification conditions by defining inference rules free from loop invariants. We further needs to improve the efficiency of the generation and expand the expressivity of the language.
若手研究(B)
研究期間:2009~2010
課題番号:21700025
研究者番号:60452116
研究分野:形式検証技術
科研費の分科・細目:情報学・ソフトウェア
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/9795
一次資料へのリンクURLhttps://dspace.jaist.ac.jp/dspace/bitstream/10119/9795/1/21700025seika.pdf
連携機関・データベース国立情報学研究所 : 学術機関リポジトリデータベース(IRDB)(機関リポジトリ)
提供元機関・データベース北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ