論文誌

[1] 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.

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

国際会議

[1] 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]

[2] 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]

[3] 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]

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

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

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

学位論文

[1] 榛葉　浩章, "JavaにおけるequalsメソッドとhashCodeメソッドの整合性の検査," 修士学位論文, 大阪大学, 2014年. [main.pdf]

[2] Yuko Muto, "Variable Coverage: a Metric to Evaluate the Exhaustiveness for Program Specifications Based on Dbc," Master thesis, Osaka University, 2012.

[3] , 仕様記述言語JMLとAlloy を用いた在庫管理プログラムの設計に対するモデル検査ツールによる検証事例, 2007. [0]