教員情報詳細
		
		
	
	
高田 喜朗TAKATA Yoshiaki
- 1969年生まれ 男性
 - 職位: 教授
 - 所属:
 - researchmap: https://researchmap.jp/read0119489
 
				
					情報学群
					
						
大学院工学研究科 基盤工学専攻 情報システム工学コース
大学院工学研究科 基盤工学専攻 情報学コース
			大学院工学研究科 基盤工学専攻 情報システム工学コース
大学院工学研究科 基盤工学専攻 情報学コース
教員略歴
| 学位 | 博士 (工学) | |
|---|---|---|
| 学歴 | 大阪大学大学院基礎工学研究科物理系専攻情報工学分野 修了(1997) | |
| 職歴 | 
					
						奈良先端科学技術大学院大学情報科学研究科助手(1997~2007)
						
							 日本電気株式会社インターネットシステム研究所客員研究員併任(2001~2007)  | 
				|
| 資格 | ||
| 専門分野 | ソフトウェアの形式モデルと検証 | |
| 研究室 | 名称 | ソフトウェア検証・解析学研究室 | 
| 詳細 | 世の中のさまざまな場所・場面でソフトウェアが利用されています。一見正しく動作しているようでも、偶然が重なったときに突如不具合を起こしたり停止したりするのでは困ります。本研究室では、ソフトウェアが正しく動作することを厳密に確かめる方法や、そのような検証がしやすい仕様記述法について研究しています。 | |
| 所属学会 | 
					
						情報処理学会
						
							 電子情報通信学会  | 
				|
横スワイプで表の続きをご覧いただけます。
本年度担当講義
| 学部・学群 | ソフトウェア工学 / 情報学群実験第2 / 情報学群セミナー / プロジェクト研究1 / 卒業研究 / プロジェクト研究2 / プロジェクト研究3 / ソフトウェア工学演習 / 工学概論 / オートマトンと形式言語 | 
|---|---|
| 大学院 | 特別研究 / 特別セミナー1 / 特別セミナー2 / 計算理論 / 情報学先端セミナー1 / 情報学先端セミナー2 | 
横スワイプで表の続きをご覧いただけます。
研究シーズ
| 相談可能な領域 | 
					
						計算機システムの数理的仕様記述
						
							 数理的検証法  | 
				
|---|---|
| 現在の研究 | 
					
						
						
							言語ベースアクセス制御付きプログラムのモデル検査法
						
						
							 XMLデータベースのアクセス制御モデル  | 
				
メッセージ
研究業績
主な受賞歴など
- 電子情報通信学会ソフトウェアサイエンス研究会研究奨励賞(2022) 電子情報通信学会ソフトウェアサイエンス研究専門委員会
 - Best Paper Award(2019) 16th International Colloquium on Theoretical Aspects of Computing (ICTAC 2019)
 
代表的な研究論文
| タイトル | 著者 | 発表誌 | 発表年 | 
|---|---|---|---|
| Non-Cooperative Rational Synthesis Problem for Probabilistic Strategies | So Koide,Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E108-D,No.7,pp.849-852 | 2025 | 
| Strategies and Equilibria on Indistinguishability of Winning Objectives and Related Decision Problems | Rindo Nakanishi,Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E108-D,No.3,pp.239-251 | 2025 | 
| A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata | Yoshiaki Takata,Akira Onishi,Ryoma Senda,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E107-D,No.12,pp.1529-1532 | 2024 | 
| Non-Cooperative Rational Synthesis Problem on Stochastic Games for Positional Strategies | So Koide,Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E107-D,No.3,pp.301-311 | 2024 | 
| A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Register Automata | Yoshiaki Takata,Akira Onishi,Ryoma Senda,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E106-D,No.3,pp.294-302 | 2023 | 
| Pumping Lemmas for Languages Expressed by Computational Models with Registers | Rindo Nakanishi,Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E106-D,No.3,pp.284-293 | 2023 | 
| Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking | Yoshiaki Takata,Ryoma Senda,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E105-D,No.9,pp.1620-1623 | 2022 | 
| Complexity Results on Register Context-Free Grammars and Related Formalisms | Ryoma Senda,Yoshiaki Takata,Hiroyuki Seki | Theoretical Computer Science,Vol.923,pp.99-125 | 2022 | 
| LTL Model Checking for Register Pushdown Systems | Ryoma Senda,Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E104-D,No.12,pp.2131-2144 | 2021 | 
| 不揮発性メモリを用いたJavaオブジェクト永続化のオーバヘッドの調査 | 松本 康太郎,高田 喜朗,鵜川 始陽 | コンピュータソフトウェア,Vol.38,No.2,pp.14-19 | 2021 | 
| Forward Regularity Preservation Property of Register Pushdown Systems | Ryoma Senda,Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E104-D,No.3,pp.370-380 | 2021 | 
| Optimal Run Problem for Weighted Register Automata | Hiroyuki Seki,Reo Yoshimura,Yoshiaki Takata | Theoretical Computer Science,Vol.850,pp.185-201 | 2021 | 
| Generalized Register Context-Free Grammars | Ryoma Senda,Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E103-D,No.3,pp.540-548 | 2020 | 
| A Formal Verification of a Subset of Information-Based Access Control Based on Extended Weighted Pushdown System | LAMILLA ALVAREZ Pablo,TAKATA, Yoshiaki | IEICE Transactions on Information and Systems,Vol.E97-D,No.5,pp.1149-1159 | 2014 | 
| Automatic Generation of History-Based Access Control from Information Flow Specification | Yoshiaki Takata,Hiroyuki Seki | 8th International Symposium on Automated Technology for Verification and Analysis (ATVA 2010), Lecture Notes in Computer Science 6252,pp.259-275 | 2010 | 
| Formal Language Theoretic Approach to the Disclosure Tree Strategy in Trust Negotiation | Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E92-D,No.2,pp.200-210 | 2009 | 
| Comparison of the Expressive Power of Language-based Access Control Models | Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E92-D,No.5,pp.1033-1036 | 2009 | 
| New Certificate Chain Discovery Methods for Trust Establishment in Ad Hoc Networks and Their Evaluation | Hisashi Mohri,Ikuya Yasuda,Yoshiaki Takata,Hiroyuki Seki | 情報処理学会論文誌,Vol.49,No.1,pp.362-374 | 2008 | 
| 実行履歴に基づくアクセス制御の形式モデルと検証 | 高田 喜朗,王 静,関 浩之 | 電子情報通信学会論文誌D,Vol.J91-D,No.4,pp.847-858 | 2008 | 
| A Labeled Transition Model A-LTS for History-Based Aspect Weaving and Its Expressive Power | Isao Yagi,Yoshiaki Takata,Hiroyuki Seki | IEICE Transactions on Information and Systems,Vol.E90-D,No.5,pp.799-807 | 2007 | 
| XML文書に対するアクセシビリティガイドライン適合性検証 | 高田 喜朗,中村 岳志,関 浩之 | 電子情報通信学会論文誌D,Vol.J89-D,No.4,pp.705-715 | 2006 | 
| A Static Analysis using Tree Automata for XML Access Control | Isao Yagi,Yoshiaki Takata,Hiroyuki Seki, | コンピュータソフトウェア,Vol.23,No.3,pp.51-65 | 2006 | 
| HBAC: A Model for History-based Access Control and Its Model Checking | Jing Wang,Yoshiaki Takata,Hiroyuki Seki | 11th European Symposium On Research In Computer Security (ESORICS 2006), Lecture Notes in Computer Science 4189,pp.263-278 | 2006 | 
横スワイプで表の続きをご覧いただけます。
学会発表・講演など
- セグメント情報のない立体ピクロス及び高さ1の立体ピクロスのNP完全性,情報処理学会第36回ゲーム情報学研究会(2016)
 - 8th International Symposium on Automated Technology for Verification and Analysis,(2010)
 - 第12回日本ソフトウェア科学会プログラミングおよびプログラミング言語ワークショップ,(2010)
 
科学研究費
KAKENは国立情報学研究所が行っているサービスです。
| 区分 | 研究課題 | 研究種目 | 研究期間 | 課題番号 | 
|---|---|---|---|---|
| 代表 | マルチスレッド再帰プログラムの自動検証のための形式モデル | 若手研究(B) | 2009 - 2010 | 21700045 | 
| 代表 | アクターモデル型マルチスレッド再帰プログラムのモデル検査法の開発 | 基盤研究(C) | 2024 - 2026 (予定) | 24K14901 | 
| 分担 | グラフゲームにおける合理性に基づく検証と自動合成の統一的解決法に関する研究 | 基盤研究(C) | 2025 - 2028 (予定) | 25K15055 | 
横スワイプで表の続きをご覧いただけます。
社会貢献及び広報活動
学外委員・学会活動など
- 情報処理学会 情報処理学会四国支部支部委員(2024~2026)
 - 電子情報通信学会 電子情報通信学会ソフトウェアサイエンス研究専門委員会副委員長(2024~2026)
 - 電子情報通信学会 電子情報通信学会四国支部支部委員(2024~2026)
 - 電子情報通信学会 電子情報通信学会ソフトウェアサイエンス研究専門委員会委員(2022~2024)
 - 情報処理学会 情報処理学会四国支部 支部幹事(2022~2024)
 - 電子情報通信学会 電子情報通信学会ソフトウェアサイエンス研究専門委員会幹事(2010~2014)
 - 電子情報通信学会 電子情報通信学会四国支部会計幹事(2009~2011)
 
一般講演など
- プログラムってなに?,
 
横スワイプで表の続きをご覧いただけます。

