高階文法を使ったオブジェクト指向プログラム検証
Verifying Object-Oriented Programs with Higher-Order Recursion Scheme
概要
ソフトウェア開発の規模が大きくなるともに一定の品質を確保することが難しくなっている。 ソフトウェアモデル検査はシステムの設計と仕様を機械的に探索することで、不具合の検出をソフトウェア開発の上流工程で可能とし、不具合の修正のための後戻りに生じるコストを大きく削減できる。 本研究では高階再帰文法を用いたモデル検査手法を拡張し、オブジェクト指向言語で書かれたプログラムの検証器の実装を行う。
産業界への展開例・適用分野
大規模なソフトウェア開発をオブジェクト指向言語で行うソフトウェア業界の品質保証に掛るコストの削減
研究者
| 氏名 | 専攻 | 研究室 | 役職/学年 |
|---|---|---|---|
| 中野 宣昭 | 知能情報学専攻 | ソフトウェア基礎論分野 | 修士2回生 |
| 五十嵐 淳 | 知能情報学専攻 | ソフトウェア基礎論分野 | 准教授 |