| 研究課題/領域番号 |
25730040
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2015年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2014年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円)
2013年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
|---|
| キーワード | ハイブリッドシステム / プログラム検証 / 不変条件 / 無限小プログラミング / 超準解析 / 次元解析 / 非線形不変条件 / システム検証 / 形式手法 / 形式検証 / プログラミング言語 / プログラミング言語理論 / プログラム意味論 / プログラム理論 |
|---|
| 研究成果の概要 |
無限小プログラミングに基づくハイブリッドシステム検証手法について研究を行った．ハイブリッドシステム検証手法としては未だ発展途上であるものの，その過程で非線形な不変条件の高速な生成手法という重要な知見が得られた．不変条件生成手法はプログラム検証において検証の成否を握る重要な要素技術であるが，既存の手法は非線形な不変条件を効率よく生成することが難しいことが多く，複雑なシステムの検証に困難が生じていた．本手法では次元解析の手法を用いることで，既存の非線形不変条件生成手法を高速化することが可能となった．研究期間終了後は本手法をさらに発展させ，より複雑なハイブリッドシステム検証手法につなげる予定である．
|
