修士（工学）, 大阪大学

博士(工学), 大阪大学

ソフトウェア, ソフトウェア工学

2020年
信州大学工学部教授

2015年 - 2020年
信州大学工学部准教授

2011年 - 2012年
大阪大学教育実践センター准教授（兼任）

2007年 - 2015年
大阪大学大学院情報科学研究科准教授（職名改正）

2007年 - 2007年
大阪府立大学理学部　非常勤講師

2002年 - 2003年
文部科学省在外研究

2002年 - 2007年
大阪大学大学院情報科学研究科助教授

1999年 - 2002年
大阪大学大学院基礎工学研究科講師

1997年 - 1999年
大阪大学大学院基礎工学研究科助手（大学院重点化）

1993年 - 1997年
大阪大学基礎工部助手

1995年, 大阪大学, 大学院基礎工学研究科, 物理系専攻　情報工学分野 (論文博士)

1993年, 大阪大学, 大学院基礎工学研究科, 物理系専攻　情報工学分野 (文部教官助手採用のため退学)

1992年, 大阪大学, 大学院基礎工学研究科, 物理系専攻　情報工学分野 (修了)

1990年, 大阪大学, 基礎工学部, 情報工学科

2022年 - 2024年
ソフトウェアサイエンス研究会専門委員長, 電子情報通信学会

2020年 - 2022年
ソフトウェアサイエンス研究会専門副委員長, 電子情報通信学会

2022年
電子情報通信学会 ソフトウェアサイエンス研究会, 電子情報通信学会 ソフトウェアサイエンス研究会 研究奨励賞

2017年
International Workshop on Informatics, Excellent Paper Award

2016年
電子情報通信学会 情報・システムソサエティ 活動功労賞

2015年
電子情報通信学会 情報・システムソサエティ論文編集活動感謝状

2015年
IPA/SEC 論文賞2014年度SEC所長賞

2010年
International Workshop on Informatics. Bet Paper Award

2008年
情報処理学会組み込みシステムシンポジウム奨励賞

1997年
情報処理学会大会優秀賞

Verification of Shell Script Behavior by Comparing Execution Log
Hitoshi Kiryu, Satoshi Suda, Shinpei Ogata, Kozo Okan
International Journal of Informatics Society, 14(2), 55-64, 2022年10月

Executable Counterex- ample for Java Model Checker
Chellet Marwan Bernard Hassan, Shinpei Ogata, Kozo Okano
International Journal of Informatics Society, 13(3), 107-113, 2022年05月

可読性の高いクラス図レイアウトを作成するための美的基準の調査
大宮拓馬, 小形真平, 岡野浩三
コンピュータソフトウェア, 38(4), 33-39, 2022年04月

Proposal and Evaluation for A Method to Verify Equivalence of Specifications of C and Java Functions with Recursive Data Structures by SAW: Case Studies of Linear Structures and Binary Trees
Rin Karashima, Kozo Okano, Shinpei Ogata, Satoshi Harauchi, and Toshifusa Sekizawa
International Journal of Informatics Society, 12(3), pp.143-156, 2021年03月

Regression Verification for C Functions with Recursive Data Structure
Kozo Okano, Rin Karashima, Satoshi Harauchi, and Shinpei Ogata
11(2), pp.107-115, 2019年10月

Consistency Checking between Java Equals and hashCode Methods Using Software Analysis Workbench
Kozo Okano, Satoshi Harauchi, Toshifusa Sekizawa, Shinpei Ogata, and Shin Nakajima
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E102(8), pp.1419-1422, 2019年08月

Effective Derivation of a Mapping of Variables in a Loop Structure
Kozo Okano, Shinji Kusumoto, and Yukihiro Sasaki
International Journal of Informatics Society, 10(2), pp.75-83, 2018年09月

Analysis of Specification in Japanese using Natural Language Processing
Kozo Okano, Kazuma Takahashi, Shinpei Ogata, and Toshifusa Sekizawa
Proceedings of the 12th Joint Conference on Knowlage-Based Software Engineering, pp.12-21, 2018年08月

Support Tool for Refining Conceptual Model in Collaborative Learning
Misaki Maruyama, Shinpei Ogata, Kozo Okano, and Mizue Kayama
Proceedings of the 12th Joint Conference on Knowlage-Based Software Engineering, pp.168-167, 2018年08月

STAMP海外事例の紹介: STPA-SafeSec
岡本圭史, 岡野浩三
SEC Journal, 13(4), pp.42-47, 2018年04月

Removing Ambiguous Message Exchanges in Designing Sequence
Satoshi Harauchi, Kozo Okano, and Shinpei Ogata
International Journal of Informatics Society, 9(3), pp.129-138, 2017年12月

On the Generation of Human-oriented Counter-examples using a Test Automaton,
Chikyu Yanagisawa, Shinpei Ogata, Kozo Okano
International Journal of Informatics Society, 9(1), pp.41-50, 2017年06月01日

Parallel Multiple Counter-Examples Guided Abstraction Loop –Applying to Timed Automaton–
Kozo Okano, Takeshi Nagaoka, Toshiaki Tanaka, Toshifusa Sekizawa, Shinji Kusumoto
International Journal of Informatics Society, 8(2), pp.103-116, 2016年04月01日

契約を用いたソフトウェア開発の修正傾向調査
岡野浩三, 吉岡一樹, 楠本真二
SEC Journal, 11(3), pp.8-15, 2016年01月01日

ソフトウェア文書匿名化ツールの試作
江川翔太, 岡野浩三, 楠本真二
電子情報通信学会論文誌, J98D(11), pp.1419-1422, 2015年11月01日

Formal Verification Technique for Consistency Checking between equals and hashCode Methods in Java
Kozo Okano, Hiroaki Shimba, Takafujmi Ohta, Hiroki Onoue, and Shinji Kusumoto
International Journal of Informatics Society, 7(2), pp.77-87, 2015年08月01日

ソースコードからのプラットフォーム依存部抽出手法
岡本周之 , 藤原貴之, 岡野浩三, 楠本真二
SEC Journal, 10(5), 8-17, 2015年01月

Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects
Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, and Shinji Kusumoto
International Journal of Informatics Society, 6(2), 79-87, 2014年

New Metrics for Program Specifications Based on DbC
Kozo Okano, Yuko Muto, Yukihiro Sasaki, Takafumi Ohta, and Shinji Kusumoto
International Journal of Informatics Society, 6(2), 79-87, 2014年

PDGとSMTソルバを利用した表明自動導出手法の提案と評価(ソフトウェア工学,<特集>ソフトウェア基礎・応用論文)
小林和貴, 佐々木幸広, 岡野浩三, 楠本真二
電子情報通信学会論文誌. D, 情報・システム, 96(11), 2657-2668, 2013年11月

Verification of Safety Properties of a Program for Line Tracing Robot using a Timed Automaton Model
Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto
International Journal of Informatics Society, 5(3), 147-155, 2013年

Implementation of a Prototype Bi-directional Translation Tool between Ocl and Jml
Kentaro Hanada, Hiroaki Shimba, Kozo Okano, and Shinji Kusumoto
International Journal of Informatics Society, 5(2), 89-96, 2013年

Alloy Analyzerを用いた表明に関する欠陥の検出手法 —JMLによる表明記述に対して—
森恵弥佳, 岡野浩三, 楠本真二
コンピュータ ソフトウェア, 30(3), 3_187-3_193, 2013年

LASP --- a Learning Assistant System for Formal Proof
Kiyoyuki Miyazawa, Kozo Okano, and Shinji Kusumoto
International Journal of Informatics Society, 4(2), 85-92, 2012年

QoS Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation
Takeshi Nagaoka,, Akihiko Ito, KozoOkano, and Shinji Kusumoto
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E94D(5), 958-966, 2011年05月

QoS Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation
Takeshi Nagaoka, Akihiko Ito, Kozo Okano, and Shinji Kusumoto
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E94D(5), 958-966, 2011年05月

A Visualization TEchnique for Unit Testing and Static Checking with Caller-Callee Relationships
Yuko Muto, Kozo Okano, and Shinji Kusumoto
Journal of Convergences, 2(2), 1-8, 2011年02月

A Model Abstraction Technique for Probabilistic Real-Time Systems Based on CEGAR for Timed Automata
Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, and Shinji Kusumoto
International Journal of Informatics Society, 3(1), 11-20, 2011年

Daikon生成表明改善のためのテストケース自動生成手法とその評価実験
宮本敬三, 堀直哉, 岡野浩三, 楠本真二
コンピュータ ソフトウェア, 28(4), 306-317, 2011年

An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
Takeshi Nagaoka, Kozo Okano, and Shinji Kusumoto
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E93D(5), 994-1005, 2010年05月

An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
Tekeshi Nagaoka, Kozo Okano, and, Shinji Kusumoto
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E93D(5), 994-1005, 2010年05月

メソッドの自動生成を用いたOCLのJMLへの変換
尾鷲方志, 岡野浩三, 楠本真二
コンピュータ ソフトウェア, 27(2), 106-111, 2010年

Stepwise Approach to Design of Real-Time Systems based UML/OCL with Formal Verification
Takeshi Nagaoka, Eigo Nagai, Toshiaki Tanaka, Kozo Okano, and Shinji Kusumoto
International Journal of Informatics Society, 1(2), 33-44, 2009年

Javaに対するループインバリアントを含むDaikon生成アサーションの妥当性評価(研究速報)
宮本敬三, 岡野浩三, 楠本真二
電子情報通信学会論文誌. D, 情報・システム, 91(11), 2721-2723, 2008年11月01日

在庫管理プログラムの設計に対するJML記述とESC/Java2を用いた検証の事例報告(研究速報)
尾鷲方志, 岡野浩三, 楠本真二
電子情報通信学会論文誌. D, 情報・システム, 91(11), 2719-2720, 2008年11月01日

上位設計におけるシステムの振る舞い検証技術
岡野浩三
システム制御情報学会誌, 52(9), 328-333, 2008年09月15日

制約指向に基づいたUMLモデルの不整合検出・解消手法の提案(ソフトウェア,<特集>フォーマルアプローチ論文)
佐々木亨, 岡野浩三, 楠本真二
電子情報通信学会論文誌. D, 情報・システム, 90(4), 1005-1013, 2007年04月01日

時間制約を保証するUML/OCLを用いた分散実時間アプリケーション開発手法(ソフトウェア,<特集>フォーマルアプローチ論文)
長井栄吾, 牧寺彩, 岡野浩三, 谷口健一
電子情報通信学会論文誌. D, 情報・システム, 89(4), 683-692, 2006年04月01日

A Timed Automata Approach to QoS Resolution
Behzad Bordbar, Rachid Anane, and Kozo Okano
International Journal of Simulation Systems, Science & Technology Special Issue on: Performance Evaluation of Computer Systems, 7(1), 46-54, 2006年

外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
竹中崇, 岡野浩三, 東野輝夫, 谷口健一
電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理, 87(4), 462-470, 2004年04月01日

凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用
柴田直樹, 岡野浩三, 谷口健一
電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理, 84(7), 999-1008, 2001年07月01日

CPU設計導入教育への形式的設計検証手法の適用
北浜優子, 北嶋暁, 岡野浩三, 谷口健一
情報処理学会論文誌, 41(11), 3114-3121, 2000年11月15日

冠頭標準形有理数プレスブルガー文の真偽判定アルゴリズムの提案
柴田直樹, 岡野浩三, 東野輝夫, 谷口健一
電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理, 82(6), 691-700, 1999年06月25日

時間ペトリネットの拡張モデルを用いたプロトコル合成
山口弘純, 岡野浩三, 東野輝夫, 谷口健一
情報処理学会論文誌, 39(3), 769-778, 1998年03月15日

遷移の選択が状態訪問回数で決まる有限状態機械対からなる通信系に対する生存性の検証
水野健太郎, 中田明夫, 岡野浩三, 東野輝夫, 谷口健一
情報処理学会論文誌, 39(3), 750-759, 1998年03月15日

共有メモリ型並列計算機上での正則な項書換え系の一実装法
松石航也, 服部哲, 岡野浩三, 東野輝夫, 谷口健一
電子情報通信学会論文誌. D-I, 情報・システム, I-コンピュータ, 81(1), 28-37, 1998年01月25日

レジスタ付きペトリネットを用いた全体動作仕様から分散動作仕様の自動合成とその応用 (<小特集>コンカレント・コラボレーション技術論文小特集)
山口弘純, 岡野浩三, 東野輝夫, 谷口健一
電子情報通信学会論文誌. A, 基礎・境界, 80(7), 1064-1072, 1997年07月25日

あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法
岡野浩三, 東野輝夫, 谷口健一
電子情報通信学会論文誌. D-I, 情報・システム, I-コンピュータ, 78(7), 622-633, 1995年07月25日

グル-プワ-クを考慮した協調計算システムにおける動作プログラム群の生成と分散実行
伊東達雄, 今城広志, 岡野浩三, 東野輝夫, 松浦敏雄, 谷口健一
情報処理学会論文誌, 36(6), 1367-1378, 1995年06月15日

関係デ-タベ-スを用いた在庫管理プログラムの記述とその詳細化の正しさの証明
森岡 澄夫; 岡野 浩三; 東野 輝夫; 谷口 健一;
情報処理学会論文誌, 36(5), 1091-1103, 1995年05月15日

リンクの故障を考慮に入れた分散システムの動作仕様の自動導出
岡野浩三, 今城広志, 東野輝夫, 谷口健一
情報処理学会論文誌, 36(1), 70-83, 1995年01月15日

Synthesis of Protocol Specifications from Service Specifications of Distributed Systems in a Marked Graph Model
Hirozumi Yamaguchi, Kozo Okano, Teruo Higashino, and Kenichi Taniguchi
IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTONICS, COMMUNICATIONS AND COMPUTER SCIENCES, E77-A(10), 1623-1633, 1994年

順序機械型プログラムの階層的設計法と在庫管理プログラムの開発例
岡野浩三, 北道淳司, 東野輝夫, 谷口健一
電子情報通信学会論文誌. D-I, 情報・システム, I-コンピュータ, 76(7), 354-363, 1993年07月25日

拡張有限状態機械モデルを用いた分散システムの要求仕様から各ノードの動作仕様の自動導出
岡野浩三, 今城広志, 東野輝夫, 谷口健一
情報処理学会論文誌, 34(6), 1290-1301, 1993年06月15日

STAMP/STPA とモデル検査の併用による単線鉄道踏切例題の 解析の効果について
岡野浩三, 岡本圭史, 小形真平
日本信頼性学会誌「信頼性」, 41(2), pp.89-96, 2019年03月

Special Section on Formal Approach FOREWORD
Kozo Okano
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E98D(6), 1120-1120, 2015年06月

システム技術に基づく安全設計ガイド
兼本 茂 , 余宮 尚志, 入月 康晴, 長久保 隆一, 三原 幸博, 岡本 圭史, 岡野 浩三
電波新聞社, 2019年

アサーションベース設計
Harry D. Foster, Adam C. Krolnik, David J. Lacey著 後藤謙治 [ほか] 訳
丸善, - 2004年
ISBN:4621074490

Reducing Syntactic Complexity for Information Extraction from Japanese Requirement Specifications
Maiko Onishi, Shinpei Ogata, Kozo Okano, Daisuke Bekki
Proceedings of 29th Asia-Pacific Software Engineering Conference (APSEC 2022), 2022年12月

Improve Measuring Suspiciousness of Bugs in Spectrum-Based Fault Localization With Deep Learning
Hitoshi Kiryu, Shinpei Ogata, and Kozo Okano
Proceedings of International Workshop on Informatics 2022, 2022年09月

A Method for Matching Patterns Based on Event Semantics with Requirements
Maiko Onishi, Shinpei Ogata, Kozo Okano, Daisuke Bekki
Proceedings of 14th International Joint Conference on Knowledge-Based Software Engineering (JCKBSE 2022), 2022年09月

Proposal of Extracting State Variables and Values from Requirement Specifications in Japanese by using Depen- dency Analysis,
Masanosuke Ohto, Hiroya Ii, Kozo Okano, and Shinpei Ogata
Proceedings of the 25th International Conference on Knowledge-Based and Intelligent Information & Engineering Systems, 2021年09月

Software edutainment systems and analysis of learners’ data based docker and edutainment
Ryosuke Tsutsumi, Jiujun Wei, Shinpei Ogata, Masaaki Niimura, and Kozo Okano
Proceedings of International Workshop on Informatics 2021, 2021年09月

可読性の高いクラス図レイアウトを作成するための美的基準の調査
大宮拓馬, 小形真平, 岡野浩三
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第 27 回ワークショップ FOSE2020, 2020年12月

Random Forest によるユーザの操作慣れ判定手法の提案
齋藤侑, 小形真平, 岡野浩三
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第 27 回ワークショップ FOSE2020, 2020年12月

モデル検査における複雑な検査式に対する反例解析手法の提案
大池勇太郎, 小形真平, 青木善貴, 中川博之, 小林一樹, 岡野浩三
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第 27 回ワークショップ FOSE2020, 2020年12月

Edutainment を指向したソフトウェア教育用フレームワークの提案
堤 崚介, 魏 久竣, 岡野浩三, 小形真平, 新村正明
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第 27 回ワークショップ FOSE2020, 2020年12月

Deriving of Time Constants in Timed Automata for Hazard Transition Sequences for STAMP/STPA
Kozo Okano, Pan Yang, Shinpei Ogata, Keishi Okamoto
Proceedings of the 23rd International Conference on Knowledge-Based and Intelligent Information & Engineering Systems,, 2020年09月

Java model check- ing: improvement of the understanding of counterexample,
Marwan Bernard Hassan Chellet, Shinpei Ogata, and Kozo Okano
Proceedings of International Workshop on Informatics 2020, 2020年09月

Improving Accuracy of Automatic Deriva- tion of State Variables and Transitions from a Japanese Requirements Specification
Hiroya Ii, Kozo Okano, and Shinpei Ogata
Proceedings of the 13th International Joint Conference on Knowledge-Based Software En- gineering, 2020年09月

STAMP/STPAとモデル検査の連携によるハザード遷移系列の導出手法
楊 盼, 岡野浩三, 小形真平, 岡本圭史
電子情報通信学会技術研究報告, SS2019, 2020年03月

Eclipse CheとDockerを用いたクラウドIDEによるプログラミング演習環境の構築
杉野雄大, 新村正明, 岡野浩三, 小形真平
電子情報通信学会技術研究報告, KBSE2019, 2020年03月

安全性解析支援のための状態遷移系に基づくハザード近接状態分析手法の提案
鈴木悠介, 小形真平, 大池勇太郎, 青木善貴, 中川博之, 小林一樹, 岡野浩三
電子情報通信学会技術研究報告, KBSE2019, 2020年03月

Edutainmentを指向したソフトウェア教育用フレームワークの提案
杉野雄大, 小形真平, 新村正明, 岡野浩三
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会 第26回ワークショップ FOSE 2019, レクチャーノート・ソフトウェア学 45 ソフトウェア工学の基礎XXVI, 2019年12月

ある組込みシステムの開発と検証のケーススタディ
岡野浩三, 小形真平, 夏目実希
電子情報通信学会技術研究報告, KBSE2019-30, 2019年11月

不具合原因分析支援のためのNuSMV反例解析手法の試案
大池勇太郎, 小形真平, 青木善貴, 中川博之, 小林一樹, 岡野浩三
電子情報通信学会技術研究報告, KBSE2019-30, 2019年11月

word2vecとゴールモデルの階層性を利用した類似ゴール検出方法の提案
石川公一, 小形真平,中川博之, 岡野浩三
電子情報通信学会技術研究報告, KBSE2019-30, 2019年11月

Automated inspection method for a STAMP/STPA – Fallen Barrier Trap at Railroad Crossing –,
Yang Pan, Kozo Okano, and Shinpei Ogata
Proceedings of the 23rd International Conference on Knowledge-Based and Intelligent Information & Engineering Systems, 2019年09月

A Review Assistance System for Class Diagram with Voice Assistance based on NLP
Masashi Nakamura, Shinpei Ogata, Kozo Okano, Toshifusa Sekizawa
Proceedings of International Workshop on Informatics 2019, 2019年09月

Proposal and evaluation for property verification for Java functions with recursive data structures by SAW
Rin Karashima, Satoshi Harauchi, Shinpei Ogata, and Kozo Okano
Proceedings of International Workshop on Informatics 2019, 2019年09月

Approach to Testing Many State Machine Models in Education
Shinpei Ogata, Mizue Kayama, Kozo Okano:
Proceedings of the 11th International Conference on Computer Supported Education (CSEDU 2019), 2019年05月

学習済みWebサイトの操作ログに基づく有効性・効率性評価の実践
青木亮太, 小形真平, 岡野浩三
電子情報通信学会技術研究報告, KBSE2018-64, 2019年03月

再帰的な構造体を用いたプログラムに対するSAWを用いた振る舞い等価性検証手法の考案と評価
辛島 凛, 原内 聡, 小形真平, 岡野浩三
第15回ソフトウェア工学の基礎ワークショップ FOSE 2018, 2018年12月

ネットワーク図のモデル化とエディタの試作 ～ より円滑なネットワークインフラの運用に向けて ～
中島徳雅, 鈴木彦文, 小形真平, 岡野浩三
電子情報通信学会技術研究報告IN pp.117-122, 2018年11月

Applying SAW to regression verification for C functions with recursive data structure
Kozo Okano, Satoshi Harauchi
Proceedings of IWIN2018, 2018年09月

Tool to Automatically Generate a Screen Transition Model Based on a Conceptual Model
Yukiya Yazawa, Shinpei Ogata, Kozo Okano, Haruhiko Kaiya, and Hironori Washizaki
Proceedings of the 12th Joint Conference on Knowlage-Based Software Engineering, 2018年08月

Towards Verification of Robot Design for Self-localization
Ryo Watanabe, Kozo Okano, and Toshifusa Sekizawa
Proceedings of 13th Haifa Verification Conference, 2017年11月

A rule-based method of stepwise evaluating class diagrams
Shinpei Ogata, Kazune Miyajima, Mizue Kayama, and Kozo Okano
Proceedings of IWIN2017, 2017年09月

A method for verifying equivalence of functions in C language,
Satoshi Harauchi, Kozo Okano, and Shinpei Ogata
Proceedings of International Workshop on Informatics 2017, 2017年09月

Derivation of a map of variables in a loop structure
Kozo Okano, Shinji Kusumoto, and Yukihiro Sasaki
Proceedings of International Workshop on Informatics 2017, 2017年09月

Equivalence Checking of Java Methods — Toward Ensuring IoT Dependability —
Kozo Okano, Satoshi Harauchi, Toshifusa Sekizawa, Shinpei Ogata, Shin Nakajima
Proceedings of The 26th International Conference on Computer Communications and Networks (ICCCN 2017), 2017年08月01日

A Method for Removing Ambiguity in Designing Sequence Diagrams for Developing Communication Programs
Kozo Okano, Satoshi Harauchi, Kozo Okano, Shinpei Ogata
Proceedings of International Workshop on Informatics 2016, 2016年09月01日

A New Proposal of Generating Counter-example in Model Checking using Test Automaton
Chikyu Yanagisawa, Shinpei Ogata, Kozo Okano
2016 pp.243-248, 2016年09月01日

Framework for Relative Web Usability Evaluation on Usability Features in MDD
Shinpei Ogata, Yugo Goto, Kozo Okano
LNCS 9856 pp.73-85, 2016年08月01日

Behavior Verification of Autonomous Robot Vehicle in Consideration of Errors and Disturbances
Toshifusa Sekizawa, Fumiya Otsuki, Kazuki Ito, and Kozo Okano
Computer Software and Applications Conference (COMPSAC) 3 550-555, 2015年07月, IEEE

Safety Verification of Multiple Autonomous Systems by Formal Approach
Kozo Okano and Toshifusa Sekizawa
LNCS 8696 11-18, 2014年09月

Verification of Spatio-Temporal Role Based Access Control using Timed Automata
Emsaieb Geepalla, Behzad Bordbar, and Kozo Okano
Proceedings of IEEE International Workshop on Design, Analysis and Tools for Integrated Circuits and Systems 1-6, 2012年

Clock Number Reduction Abstraction on CEGAR Loop Approach to Timed Automaton
Kozo Okano, Behzad Bordbar, and Takeshi Nagaoka
Prpoceedings of the 2nd International Conference on Networking and Computing, 2011年

A Method to Generate Pre- and Postconditions for Java Methods Based on Hybrid Analysis
Kozo Okano, Shinji Kusumoto, and Yasunobu Kajita
Proceedings of International Workshop on Informatics 2008, 2008年

An Evaluation Mechanism for QoS Management in Wireless Systems
Behzad Bordbar, Rachid Anane, and Kozo Okano
Proceedings of ICPADS 2005, 2005年

Testing Deadlock-freeness in Real-time Systems --- A Formal Approach ---
Behzad Bordbar and Kozo Okano
LNCS 3395 95-109, 2004年

Verification of Timeliness QoS Properties in Multimedia Systems
Behzad Bordbar and Kozo Okano
LNCS 2885 532-540, 2003年

IEEE

情報処理学会

電子情報通信学会

日本ソフトウェア科学会

自然語解析と反例解析を活用したソフトウェア開発
科学研究費補助金
2021年 - 2024年

ソフトウェア設計に関する共同研究　三菱電機（株）
受託研究, 三菱電機（株）
2021年 - 2021年03月31日

ソフトウェア設計に関する共同研究　三菱電機（株）
受託研究, 三菱電機（株）
2020年 - 2021年03月31日

プログラミング学習支援とデータ活用
受託研究, 文部科学省の「Society5.0実現化研究拠点支援事業」に基づき大阪大学が運営している「ライフデザイン・イノベーション研究拠点（iLDi）事業　グランドチャレンジ研究」
2020年 - 2021年03月31日

ソフトウェア・モデル検査における説明可能な反例生成に関わる基礎研究
共同研究, 国立情報学研究所
2020年 - 2021年

ソフトウェア設計に関する共同研究　三菱電機（株）
受託研究, 三菱電機（株）
2019年 - 2020年03月31日

プログラミング学習支援とデータ活用
受託研究, 文部科学省の「Society5.0実現化研究拠点支援事業」に基づき大阪大学が運営している「ライフデザイン・イノベーション研究拠点（iLDi）事業　グランドチャレンジ研究」
2019年 - 2020年03月31日

ソフトウェア設計に関する共同研究　三菱電機（株）
受託研究, 三菱電機（株）
2018年 - 2020年03月31日

ソフトウェア設計に関する共同研究　三菱電機（株）
受託研究, 三菱電機（株）
2018年 - 2019年03月31日

IoTソフトウェアに対する反例解析を活用した自動検証技術
共同研究, 国立情報学研究所
2018年 - 2019年

組み合わせテストを応用した組込みシステムの検証項目生成の研究
科学研究費補助金
2017年 - 2019年

ソフトウェア設計に関する共同研究　三菱電機（株）
受託研究, 三菱電機（株）
2017年 - 2018年03月31日

モテルと制約に基つくソフトウェア開発に関する研究
科学研究費 (基盤研究(C))
2016年04月 - 2019年03月

モデルと制約に基づくソフトウェア開発に関する研究
科学研究費補助金
2016年 - 2018年

ソフトウェア設計に関する共同研究　三菱電機（株）
受託研究, 三菱電機（株）
2016年 - 2017年03月31日

特定機能に着目した組込みシステムソフトウェアの安全性検証技術
共同研究, 国立情報学研究所
2016年 - 2017年

ソフトウェア設計に関する共同研究　三菱電機（株）
受託研究, 三菱電機（株）
2015年 - 2016年03月31日

動的システムに対する組込み制御プログラムの信頼性検証に関する研究
科学研究費補助金
2014年 - 2016年

多様なソフトウェア資産の収集・分析・評価と効果的な利活用の研究
科学研究費補助金
2013年 - 2017年

モデル検査技術を活用したソフトウェア設計方法に関する研究
科学研究費 (基盤研究(C))
2009年04月 - 2014年03月

モデル検査技術を活用したソフトウェア設計方法に関する研究
科学研究費補助金
2009年 - 2013年

状態爆発するWEB アプリケーションに対するソフトウェアモデル検査
科学研究費 (特定領域研究　情報爆発IT 基盤　公募研究)
2006年04月 - 2007年03月

状態爆発するWEBアプリケーションに対するソフトウェアモデル検査
科学研究費補助金
2006年 - 2006年

契約に基づいた関数型プログラム設計に対する正当性保証に関する研究
科学研究費 (若手研究(B) )
2005年04月 - 2007年03月

契約に基づいた関数型プログラム設計に対する正当性保証に関する研究
科学研究費補助金
2005年 - 2006年

関数型プログラムに対するモジュール構造を考慮に入れた効率のよい形式的検証支援
科学研究費 (若手研究(B) )
2002年04月 - 2005年03月

モデル検査を用いた要求仕様検証

2020年06月 - 2022年05月
電子情報通信学会ソフトウェアサイエンス研究会専門副委員長

2002年05月 - 2011年05月
電子情報通信学会ソフトウェアサイエンス研究会専門委員

2004年 - 2004年
ソフトウェアシンポジウムPC委員

2004年 - 2004年
LA シンポジウム事務局庶務

2005年 - 2005年
日本ソフトウェア科学会プログラミングおよびプログラミング言語ワークショップPPL PC委員

2007年 - 2012年
情報処理学会組込みシステム研究会シンポジウム ESS　PC委員

2007年 - 2012年
日本ソフトウェア科学会ソフトウェア工学の基礎研究会ワークショップ FOSE PC委員

2008年05月 - 2012年05月
情報処理学会ソフトウェア工学研究会運営委員

2008年 - 2008年
国際会議Asia-Pacific Software Engineering Conference APSEC PC委員

2009年 - 2009年
国際会議Adaptive Systems in Heterogeneous Environments ASHEs PC委員

2009年 - 2010年
国際会議Australasian Software Engineering Conference ASWEC　PC委員

2009年 - 2009年
国際会議Asia-Pacific Software Engineering Conference APSEC PC委員

2011年05月 - 2013年05月
情報処理学会ソフトウェア工学特集号編集委員

2011年05月 - 2013年05月
電子情報通信学会英文D 誌フォーマルアプローチ特集号編集委会委員

2011年05月 - 2015年05月
電子情報通信学会和文論文誌D 学生論文特集号編集委員会委員

2011年05月 - 2015年05月
電子情報通信学会和文論文誌D 編集委員会委員

2011年05月 - 2015年05月
情報処理学会論文誌ジャーナル/JIP 論文誌編集委員会委員

2012年05月 - 2014年05月
電子情報通信学会英文D 誌フォーマルアプローチ特集号編集委員会幹事

2012年 - 2013年
国際会議International Workshop on Informatics IWIN PC Chair

2012年11月 - 2013年11月
電子情報通信学会和文論文誌D システム論文特集号編集委員会委員

2013年02月 - 2013年11月
電子情報通信学会和文論文誌D ソフトウェア基礎・応用特集号 編集委員会幹事

2013年 - 2013年
情報処理学会組込みシステム研究会シンポジウム ESS　共同PC副委員長

2013年 - 2013年
日本ソフトウェア科学会ソフトウェア工学の基礎研究会ワークショップFOSE　共同PC委員長

2013年 - 2013年
日本ソフトウェア科学会 ソフトウェア工学特集号　編集委員

2014年 - 2014年
情報処理学会組込みシステム研究会シンポジウム PC委員長

2014年 - 2014年
国際会議International Workshop on Informatics IWIN General Co-Chair

2014年05月 - 2015年05月
電子情報通信学会英文D 誌フォーマルアプローチ特集号　編集委員会委員長

2015年 - 2015年
国際会議 Asia-Pacific Software Engineering Conference APSEC　PC委員

2015年 - 2015年
情報処理学会組込みシステム研究会シンポジウム ESS実行副委員長

2016年 - 2016年
国際会議International Workshop on Informatics IWIN General Co-Chair

2019年04月01日 - 2020年03月31日, 広報委員

2020年04月01日 - 2021年03月31日, 広報委員

2021年05月01日 - 2022年03月31日, 学務委員

2021年05月01日 - 2022年04月30日, 副学科長

2022年04月01日 - 2023年03月31日, 学科長

2023年04月01日, 数理DS・AI教育研究センター