|
JAIST Repository >
b. 情報科学研究科・情報科学系 >
b50. 科学研究費助成事業研究成果報告書 >
2010年度 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/9795
|
| タイトル: | データ管理領域におけるプログラム検証の自動化に関する研究 |
| その他のタイトル: | Automating program verification on the data management domain |
| 著者: | 矢竹, 健朗 |
| 著者（別表記）: | Yatake, Kenro |
| キーワード: | プログラム検証
定理証明
オブジェクト指向
データ管理領域 |
| 発行日: | 1-Apr-2011 |
| 抄録: | 本研究では、データ管理領域に焦点を当て、プログラム検証を自動化する手法を提案した。データ管理システムに特有の繰り返し処理を行う命令、推論規則を導入した言語を定義し、検証条件自動生成器を実装した。推論規則をループ不変表明に依存しないものとすることにより、検証条件の自動生成を可能とした。今後、検証条件の生成効率の改善、言語の表現力の拡張に関して検討する必要がある。 : 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. |
| 記述: | 若手研究（Ｂ）
研究期間：2009～2010
課題番号：21700025
研究者番号：60452116
研究分野：形式検証技術
科研費の分科・細目：情報学・ソフトウェア |
| 言語: | jpn |
| URI: | http://hdl.handle.net/10119/9795 |
| 出現コレクション: | 2010年度 (FY 2010)
|
このアイテムのファイル:
| ファイル |
記述 |
サイズ | 形式 |
|---|
| 21700025seika.pdf | | 182Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|
