@techreport{oai:kanazawa-u.repo.nii.ac.jp:00047640,
 month = {Apr},
 note = {リアルタイムオブジェクト指向言語を開発して、オブジェクトが生成消滅するシステムに対して、構造と時間の抽象化精錬で直接に検証できる、動的リアルタイムCEGARの開発と実装に取り組んだ。その結果、動的リアルタイムCEGARの実現により、オブジェクトの生成消滅といった構造の変化及びリアルタイム性を同時に抽象化精錬して、リアルタイムオブジェクト指向システムの効率的なモデル検査が実現できることを明らかにした。, 研究課題/領域番号:19500025, 研究期間(年度):2007-2009, 出典：研究課題「述語抽象化検証による大規模組込みシステム向きオブジェクト指向設計自動検証手法」課題番号19500025
（KAKEN：科学研究費助成事業データベース（国立情報学研究所）） 
（https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-19500025/19500025seika/）を加工して作成, 金沢大学理工研究域電子情報通信学系},
 title = {述語抽象化検証による大規模組込みシステム向きオブジェクト指向設計自動検証手法},
 year = {2010}
}