解説

[1] 岡野浩三, "時間オートマトン," 電子情報通信学会ハンドブック/知識ベース, volume 7 群1 編3 章3-2, 2010年.

[2] 岡野浩三, "上位設計におけるシステムの振る舞い検証技術," システム/制御/情報, volume Vol. 52, number No. 9, pp.328-333, 2008年9月.

論文誌

[1] 江川 翔太, 岡野 浩三, 楠本 真二, "ソフトウェア文書匿名化ツールの試作," 電子情報通信学会論文誌D, volume J98-D, number 11, pages 1419-1422, 2015年11月.

[2] 小林和貴, 佐々木幸広, 岡野浩三, 楠本真二, "PDGとSMTソルバを利用した表明自動導出手法の提案と評価," 電子情報通信学会論文誌D, volume J96-D, number 11, pages 2657-2668, 2013年11月.

[3] 森恵弥佳, 岡野浩三, 楠本真二, "Alloy Analyzerを用いた表明に関する欠陥の検出手法 -JMLによる表明記述に対して-," コンピュータソフトウェア, volume 30, number 3, pages 187-193, 2013年8月.

[4] Kentaro Hanada, Hiroaki Shimba, Kozo Okano, and Shinji Kusumoto, "Implementation of a Prototype Bi-Directional Translation Tool between Ocl and Jml," International Journal of Informatics Society (IJIS), volume 5, 2013.

[5] Takeshi Nagaoka, Akihiko Ito, Kozo Okano, and Shinji Kusumoto, "Qos Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation," IEICE Transactions on Information and Systems, volume E94-D, number 5, May 2011.

[6] 宮本敬三, 堀直哉, 岡野浩三, 楠本真二, "Daikon 生成表明改善のためのテストケース自動生成手法とその評価実験," 日本ソフトウェア科学会誌コンピュータソフトウェア, volume Vo.28, number No.4, pp.4-306-4-317, 2011年.

[7] Yuko Muto, Kozo Okano, and Shinji Kusumoto, "A Visualization Technique for Unit Testing and Static Checking with Caller-Callee Relationships," Journal of Convergences, volume 2, number 2, pages 1-8, 2011. [A101.pdf]

[8] Takeshi Nagaoka, Kozo Okano, and Shinji Kusumoto, "An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop," IEICE Transactions on Information and Systems, volume E93-D, number 5, pages 994-1005, May 2010.

[9] 尾鷲方志, 岡野浩三, 楠本真二, "メソッドの自動生成を用いたOCLのJMLへの変換," コンピュータソフトウェア, volume 27, number 2, 2010年5月. [jssst.pdf]

[10] Takeshi Nagaoka, Eigo Nagai, Kozo Okano, and Shinji Kusumoto, "Stepwise Approach to Design of Real-Time Systems Based Uml/Ocl with Formal Verification," International Journal of Informatics Society (IJIS), volume 1, number 2, pages 37-44, September 2009.

[11] 尾鷲方志, 岡野浩三, 楠本真二, "在庫管理プログラムに対するJML記述とESC/Java2を用いた検証の事例報告," 電子情報通信学会論文誌 VOL.J91-D NO.11, volume 91-D, number 11, pages 2719-2720, 2008年11月. [0]

[12] 宮本敬三, 岡野浩三, 楠本真二, "Javaに対するループインバリアントを含むDaikon生成アサーションの妥当性評価," 電子情報通信学会論文誌D, volume J91-D, number 11, pages 2721-2723, 2008年11月. [0]

表彰・受賞

[1] Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, and Shinji Kusumoto, "Iwin2010 Best Paper Award," , 2010.

[2] 長岡武志, 岡野浩三, 楠本真二, "組込みシステムシンポジウム2008 奨励賞," , 2008年10月.

国際会議

[1] Haruki Yokoyama, Yoshiki Higo, Keisuke Hotta, Takafumi Ohta, Kozo Okano, , and Shinji Kusumoto, "Toward Improving Ability to Repair Bugs Automatically –A Patch Candidate Location Mechanism Using Code Similarity–," In 31st ACM Symposium on Applied Computing, pages 1364-1370, April 2016. [y-haruki_SAC2016.pdf]

[2] Hiraoki Shimba, Takafumi Ohta, Hiroki Onoue, Kozo Okano, and Shinji Kusumoto, "Formal Verification Technique for Consistency Checking between Equals and Hashcode Methods in Java," In IWIN2014, September 2014. [desc]

[3] Hiroaki Shimba, Kentaro Hanada, Kozo Okano, and Shinji Kusumoto, "Bidirectional Translation between Ocl and Jml for Round-Trip Engineering," In 5th International Workshop on Empirical Software Engineering in Practice (IWESEP2013), pages 49-54, December 2013. [2144b049.pdf]

[4] Yuko Muto, Yukihiro Sasaki, Takafumi Ohta, Kozo Okano, Shinji Kusumoto, , and Kazuki Yoshioka, "Variable Coverage: a Metric to Evaluate the Exhaustiveness for Program Specifications Based on Dbc," International Workshop on Informatics 2013, pages 123-132, 2013. [main.pdf]

[5] Kentaro Hanada, Hiroaki Shimba, Kozo Okano, and Shinji Kusumoto , "A Bi-Directional Translation Tool between Ocl and Jml Considering Reverse Translation," In The 4th International Workshop on Empirical Software Engineering in Practice (IWESEP2012), poster presentation, October 2012.

[6] Kentaro Hanada, Hiroaki Shinba, Kozo Okano, and Shinji Kusumoto, "Implementation of a Prototype Bi-Directinal Translation Tool between Ocl and Jml," International Workshop on Informatics 2012, pages 121-127, September 2012. [iwin2012.pdf]

[7] Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto, "Verification of Safety Property of Line Tracer Program Using Timed Automaton Model," International Workshop on Informatics 2012, pages 136-142, September 2012. [iwin2012.pdf]

[8] Kentaro Hanada, Kozo Okano, Shinji Kusumoto, and Kiyoyuki Miyazawa, "Practical Application of a Translation Tool from Uml/Ocl to Java Skeleton with Jml Annotation," In 14th International Conference on Enterprise Information Systems, pages 389-394, June 2012. [document.pdf]

[9] Yuko Muto, Kozo Okano, and Shinji Kusumoto, "Improvement of a Visualization Technique for the Passage Rate of Unit Testing and Static Checking and Its Evaluation," In Proc. of the Joint Conference of the 21th International Workshop on Software Measurement and the 6th International Conference on Software Process and Product Measurement (IWSM/MENSURA2011), pages 279-284, November 2011. [document.pdf]

[10] Kiyoyuki Miyazawa, Kozo Okano, and Shinji Kusumoto, "Lasp - a Learning Assistant System for Formal Proof," In International Workshop on INformatics, IWIN 2011, pages 158-165, September 2011.

[11] Yuko Muto, Kozo Okano, and Shinji Kusumoto, "A Visualization Technique for the Passage Rate of Unit Testing and Static Checking with Caller-Callee Relationships," In International Conference on Advanced Software Engineering, pages 336-341, May 2011. [ICASE.pdf]

[12] Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, and Shinji Kusumoto, "Reachability Analysis of Probabilistic Timed Automata Based on an Abstraction Refinement Technique," Proceedings of International Workshop on Empirical Software Engineering in Practice 2010 (IWESEP 2010), pages 33-38, December 2010. [IWESEP12.pdf]

[13] Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, and Shinji Kusumoto, "Reachability Analysis of Probabilistic Real-Time Systems Based on Cegar for Timed Automata," In Proceedings of International Workshop on Informatics 2010, pages 18-26, September 2010. [IWIN2010_Number17.pdf]

[14] Takeshi Nagaoka, Akihiko Ito, Kozo Okano, and Shinji Kusumoto, "Qualitative Analysis of Real-Time Distributed Systems Considering Network Congestion by Probabilistic Model Checker Prism," In Proceedings of 2009 International Workshop on Empirical Software Engineering in Practice (IWESEP 2009), October 2009.

[15] Takeshi Nagaoka, Akihiko Ito, Kozo Okano, and Shinji Kusumoto, "Qos Evaluation for Real-Time Distributed Systems Using the Probabilistic Model Checker Prism," In Proceedings of International Workshop on Informatics 2009, pages 60-66, September 2009. [IWIN2009_NUMBER14.pdf]

[16] Takeshi Nagaoka, Kozo Okano, and Shinji Kusumoto, "Stepwise Approach to Design of Real-Time Systems Based Uml/Ocl with Formal Verification," In Proceedings of International Workshop on Informatics, pages 98-105, September 2008. [0]

国内会議(査読付き)

[1] 佐々木 幸広, 岡野 浩三, 楠本 真二, "SMTソルバと統計解析を用いたJavaプログラム解析器の提案," ソフトウェア工学の基礎XX(日本ソフトウェア科学会FOSE 2013), 2013年11月.

[2] 榛葉浩章, 岡野浩三, 楠本真二, "制約記述言語OCLとJMLの双方向変換手法の提案 ," ソフトウェア工学の基礎XX(日本ソフトウェア科学会FOSE 2013), 2013年11月. [FOSE2013Poster.pptx]

[3] 佐々木 幸広, 岡野 浩三, 楠本 真二, "SMTを活用したJava プログラム解析器の設計," ソフトウェア工学の基礎XIX, pages 33-38, 2012年12月. [fose2012.pdf]

[4] 武藤 祐子, 岡野 浩三, 楠本 真二, "呼び出し関係を用いた単体テストおよび静的検査の可視化手法の改善とその評価," ソフトウェア工学の基礎XVIII 日本ソフトウェア科学会FOSE2011, pages 163-168, 2011年11月. [paper7.pdf]

[5] 小林和貴, 宮本敬三, 岡野浩三, 楠本真二, "アサーション動的生成を目的としたテストケース制約のESC/Java2を利用した導出," 高田 眞吾,　福田 浩章(編), ソフトウェア工学の基礎XVII, number 36, pages 35-44, 2010年11月. [投稿PDF]

[6] 宮本敬三, 堀直哉, 岡野浩三, 楠本真二, 西本哲, "アサーション動的生成のためのテストケース自動生成手法の生成アサーションの妥当性評価," ソフトウェア工学の基礎XVI 日本ソフトウェア科学会FOSE2009, pages 183-190, 2009年11月. [fose2009.pdf]

[7] 尾鷲方志, 岡野浩三, 楠本真二, "メソッドの自動生成を用いたOCLのJMLへの変換ツールの設計," レクチャーノート・ソフトウェア学 35 ソフトウェア工学の基礎XVI, pages 191-198, 2009年11月. [fose.pdf]

[8] 宮澤清介, 岡野浩三, 楠本真二 , "フォーマルアプローチの基本技術習得のための学習支援システムの試作," ソフトウェアエンジニアリング最前線2009, pages 69-74, 2009年9月. [SES2009_MiyazawaKiyoyuki.pdf]

[9] 堀直哉, 岡野浩三, 楠本真二, "モデル検査技術を用いたインバリアント被覆テスト ケースの自動生成によるDaikon出力の改善," 松下 誠, 川口 真司(編), ソフトウェア工学の基礎XV 日本ソフトウェア科学会FOSE2008, pages 41-50, 2008年11月. [0]

[10] 長岡武志, 岡野浩三, 楠本真二, "時間オートマトンを対象としたコンポーネント部分合成による抽象化洗練手法の改良," 組込みシステムシンポジウム2008 論文集, volume 2008, number 9, pages 141-150, 2008年10月. [0]

研究会・全国大会等

[1] 横山 晴樹, 大田 崇史, 堀田 圭佑, 肥後 芳樹, 岡野 浩三, 楠本 真二, "再利用に基づく自動バグ修正における再利用候補の絞込に向けた調査," 電子情報通信学会技術研究報告, volume 115, number 20, pages 047-052, 2015年5月. [y-haruki_sigss2015_submit.pdf]

[2] 楠　野明, 岡野　浩三, 楠本　真二, "シーケンス図が持つメッセージ順序の曖昧性除去手法の提案," 電子情報通信学会技術研究報告, volume 114, number 510, 2015年3月. [sigss-k-noa.pdf]

[3] 江川 翔太, 岡野 浩三, 楠本 真二, ソフトウェア開発ドキュメント匿名化ツールの試作, ソフトウェア信頼性研究会第10回ワークショップ（FORCE 2014）, 2014年. [ソフトウェア開発ドキュメント匿名化ツールの試作.pdf]

[4] 江川 翔太, 岡野 浩三, 楠本 真二, ソフトウェア開発ドキュメント匿名化ツールの試作とその評価, ソフトウェア・シンポジウム2014, 2014年. [SS2014.pdf]

[5] 榛葉 浩章, 尾ノ上 博樹, 岡野 浩三, 楠本真二, "JavaにおけるequalsメソッドとhashCodeメソッドの整合性の検査手法の提案," 電子情報通信学会技術研究報告, volume 113, number 489, pages 19-24, 2014年3月. [document.pdf]

[6] 佐々木 幸広, 岡野 浩三, 楠本 真二, PDGとSMTソルバを用いたJavaプログラム解析器の提案, SESワークショップ2013, 2013年.

[7] 藤田悠矢, 岡野浩三, 楠本真二, "異なるスキーマ間に対応するSQL文の整合性のAlloy Analyzerを用いた一検証手法," 電子情報通信学会技術研究報告, volume 113, number 159, pages 007-012, 2013年7月. [sigss1307_f-yuya.pdf]

[8] 吉岡一樹, 岡野浩三, 楠本真二, "契約記述の変更傾向の開発履歴情報を用いた調査," 電子情報通信学会技術研究報告, volume 112, number 457, pages 121-126, 2013年3月.

[9] 森恵弥佳, 岡野浩三, 楠本真二, "在庫管理プログラムに対する Alloy Analyzer を用いた検証事例," 情報処理学会シンポジウムシリーズ ウィンターワークショップ2013・イン・那須, volume 2013, number 1, pages 5-6, 2013年1月. [desc]

[10] 榛葉浩章, 花田健太郎, 岡野浩三, 楠本真二, "制約記述言語OCLとJMLのモデル駆動開発技法に基づいた双方向の変換手法の提案," 電子情報通信学会技術研究報告, volume 111, number 481, 2012年3月. [document.pdf]

[11] 佐々木幸広, 小林和貴, 岡野浩三, 楠本真二, "SMTソルバーとPDG作成ツールを用いた Java のテストケース自動導出手法の提案," 電子情報通信学会技術研究報告 , volume 111 , number 481, pages 55-60, 2012年2月. [Sigss2012.pdf]

[12] 吉岡一樹, 武藤祐子, 岡野浩三, 楠本真二, "JMLによって記述された契約に対する品質評価手法の在庫管理プログラムへの適用," 情報処理学会シンポジウムシリーズ ウィンターワークショップ2012・イン・琵琶湖, volume 2012, number 1, pages 109-110, 2012年1月.

[13] 花田 健太郎, 岡野 浩三, 楠本 真二, "OCLからJMLへのDSLを用いた変換ツールの試作型の実装," 情報処理学会シンポジウムシリーズ ウィンターワークショップ2012・イン・琵琶湖, volume 2012, number 1, 2012年1月. [f05.pdf]

[14] 武藤祐子, 岡野浩三, 楠本真二, "JML によって記述された契約に対する品質評価手法 の提案," 情報処理学会関西支部支部大会, 2011年9月.

[15] 小林和貴, 岡野浩三, 楠本真二, "Daikon を利用した表明動的生成改善手法の実プロ ジェクト教材への適用実験とテストデータ生成改善手法の検討," 平成23 年度情報 処理学会関西支部支部大会,, 2011年9月.

[16] 小林和貴, 岡野浩三, 楠本真二, "モデル検査器とDaikon を用いた表明動的生成改善 手法のシステム開発実プロジェクト教材への適用と評価," 電子情報通信学会技術報告, 2011年7月.

[17] 宮澤清介, 岡野浩三, 楠本真二, "OCLのJMLへの変換ツールの実装と評価," number 170, 情報通信学会技術報告, 2010年11月. [desc]

[18] 宮澤清介, 岡野浩三, 楠本真二, "数理論理学の形式証明に対する学習支援システムの試作と評価," 情報通信学会技術報告, 2010年9月. [desc]

[19] 伊藤明彦, 長岡武志, 岡野浩三, 楠本真二, "時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析," 電子情報通信学会技術研究報告, volume 109, number 456, pages 85-90, 2010年3月. [SIGSS1003.pdf]

[20] 宮澤清介, 岡野浩三, 楠本真二, "OCLのJMLへの変換ツールの実装," number 110, 電子情報通信学会技術報告, 2010年3月. [desc]

[21] 田中俊彰, 長岡武志, 岡野浩三, 楠本真二, "実時間システムを対象としたCEGARによる抽象洗練の並列化手法," 電子情報通信学会信学技報, volume 110, number 169, pages 35-40, 2010年. [SIGSS201008tstanaka-final.pdf]

[22] 田中俊彰, 長岡武志, 岡野浩三, 楠本真二, "時間システムを対象とした到達可能性解析の高速化手法の提案," 情報処理学会研究報告, volume 170, number 15, 2010年. [SIGSE201011Ver08.pdf]

[23] 伊藤明彦, 長岡武志, 岡野浩三, 楠本真二, "確率的モデル検査ツールを用いた実時間ネットワークシステムの 検証手法の提案およびネットワークシミュレータNS-2 との比較," 電子情報通信学会技術報告, volume 109, number 170, pages 37-42, 2009年8月. [SIGSS0908.pdf]

[24] 宮本敬三, 堀直哉, 岡野浩三, 楠本真二, "Javaに対するDaikonを用いたインバリアント自動生成のための汎用基盤ツール," 第7回情報科学技術フォーラム講演論文集, 2008年8月. [0]

[25] Takeshi Nagaoka, Kozo Okano, and Shinji Kusumoto, "Abstraction of Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop," IEICE Technical Report, volume 107, number 505, pages 103-108, March 2008. [0]

[26] 長岡武志, 岡野浩三, 楠本真二, "UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法," 電子情報通信学会技術報告, volume 107, number 176, pages 77-82, 2007年8月. [0]

[27] 尾鷲方志, 岡野浩三, 楠本真二, "JMLを用いた在庫管理プログラムの設計とESC/Java2 を用いた検証," 電子情報通信学会技術報告, volume 107, number 176, pages 37-42, 2007年8月. [0]

Technical Report

[1] Takeshi Nagaoka, Kozo Okano, and Shinji Kusumoto, "An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop," Techinical Report of Software Design Lab in Osaka Univ. SDL-Sep-3-2008, 2008. [0]