Bibliography

• International
• New! Kenro Yatake and Toshiaki Aoki: Model Checking an OSEK/VDX OS Design Model based on Environment Modelling, ICTAC 2012. (full paper)
• New! Kenro Yatake and Toshiaki Aoki: Verification of an OSEK/VDX Operating System with Environment Modeling, WCEIT 2012. (presentation only)
• New! Kenro Yatake and Toshiaki Aoki: SMT-based Enumeration of Object Graphs from UML Class Diagrams, UML&FM 2012. (full paper)
• Kenro Yatake and Toshiaki Aoki: Automatic Generation of Model Checking Scripts based on Environment Modeling, Proceedings of the 17th International SPIN Workshop on Model Checking of Software, SPIN 2010, pp.58-75, 2010. (full paper) pdf
• Journal Kenro Yatake and Takuya Katayama: An executable object-oriented semantics and its application to firewall verification, Software and Systems Modeling DOI: 10.1007/s10270-010-0160-1.
• Kenro Yatake and Takuya Katayama: An executable semantics of Object-Oriented models for simulation and theorem proving, Proceedings of the 6th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2008, pp.71-80, 2008. (full paper) pdf
• Kenro Yatake, Toshiaki Aoki and Takuya Katayama: Implementing application-specific Object-Oriented theories in HOL, International Conference on Theoretical Aspects of Computing, ICTAC 2005, pp.501-516. (full paper) pdf
• Kenro Yatake, Toshiaki Aoki and Takuya Katayama: Collaboration-based Verfication of Object-Oriented models in HOL, Proceedings of the 2nd International Workshop on Verification and Validation of Enterprise Information Systems, VVEIS 2004, pp.78-80, 2004. (poster)

• Domestic
• New! Journal 矢竹健朗, 青木利晃： UMLに基づくRTOSの設計検証のための環境自動生成法, コンピュータソフトウェア, 2012.
• 矢竹健朗, 西端浩和, 青木利晃： 環境モデリングによるモデル検査スクリプトの自動生成, 情報処理学会 ソフトウェア工学の基礎ワークショップ (FOSE), 2009. pptx
• 矢竹健朗, 西端浩和, 青木利晃： 環境モデリングによるモデル検査スクリプトの自動生成, 情報処理学会 組込みシステムシンポジウム (ESS) 論文集 pp.59-64, 2009.
• 矢竹健朗： データ管理領域におけるプログラム検証の自動化に関する考察， 情報処理学会 ソフトウェア工学研究会 研究報告 2009-SE-165, 2009.
• Journal 矢竹健朗, 片山卓也： 事例研究：定理証明によるファイアウォールサーバモデルの検証, コンピュータソフトウェア, Vol.26, No.1(2009), pp.111-126.
• 矢竹健朗，片山卓也： オブジェクト列に対するループ文の推論規則， 第5回ディペンダブルソフトウェアワークショップDSW2007, 予稿集, pp.57-63. pdf
• 矢竹健朗，片山卓也： 定理証明器HOLにおけるファイアウォールサーバのセキュリティ検証， 第3回システム検証の科学技術シンポジウム2006, 予稿集, pp.59-66.
• Journal 矢竹健朗, 青木利晃, 片山卓也： コラボレーションに基づくオブジェクト指向モデルの検証, コンピュータソフトウェア, Vol.22, No.1(2005), pp.58-76.
• 矢竹健朗，青木利晃，片山卓也： 定理証明システムHOLにおけるオブジェクト指向理論の構築， 情報処理学会 ソフトウェア工学研究会 研究報告 2002-SE-138, 2002.

• Books
• 矢竹健朗：オブジェクト指向理論によるファイアウォールサーバの検証, JAIST Press, 2006.