师资信息详情

语言 ≫ 英语
高田吉明-2jpg

高田芳郎高田义明

  • 男，1969年出生
  • 职位：教授
  • 隶属关系：
    • 信息科学学院
    工学研究科基础设施工学系信息系统工学课程
    工学研究科基础设施工学系信息学课程
  • 研究地图：https://researchmapjp/read0119489

教师简历

学位 博士（工程）
学术背景 大阪大学大学院工学研究科物理系信息工程系结业（1997年）
工作经历 奈良科学技术大学信息科学研究生院助理（1997-2007）
兼任NEC互联网系统研究所客座研究员（2001-2007）
资质
专业 正式的软件建模和验证
实验室 名称 软件验证与分析实验室
详情 软件在世界各地和不同情况下使用。即使乍一看似乎工作正常，但如果由于巧合而突然发生故障或停止，那就是一个问题了。在我们的实验室中，我们正在研究严格验证软件是否正确运行的方法，以及促进这种验证的规范编写方法。
附属学术团体 日本信息处理学会
IEICE

水平滑动即可查看表格的其余部分。

今年讲授的讲座

教师/小组 软件工程/
研究生院 专题研究​/

水平滑动即可查看表格的其余部分。

研究种子

可讨论的领域 计算机系统的数学规范描述
数学验证方法
当前研究 基于语言的访问控制程序的模型检查方法

XML 数据库访问控制模型

留言

研究成果

主要奖项等

  • IEICE软件科学研究组研究鼓励奖（2022）IEICE软件科学研究专委会
  • 最佳论文奖（2019）第十六届计算理论方面国际研讨会（ICTAC 2019）

代表性研究论文

标题 作者 出版杂志 公布年份
多人游戏中受限安全均衡存在的复杂性 水野宏树、高田义明、关宏之 IEICE 信息和系统交易 2026
概率策略的非合作理性综合问题 So Koide、Yoshiaki Takata、Hiroyuki Seki IEICE 信息与系统汇刊，E108-D 卷，第 7 期，第 849-852 页 2025
关于获胜目标和相关决策问题的不可区分性的策略和均衡 Rindo Nakanishi、Yoshiaki Takata、Hiroyuki Seki IEICE 信息与系统汇刊，E108-D 卷，第 3 期，第 239-251 页 2025
Mu 微积分的子类，其冻结量词相当于 Buchi 配准自动机 高田义明、大西晃、仙田龙马、关宏之 IEICE 信息与系统汇刊，E107-D 卷，第 12 期，第 1529-1532 页 2024
位置策略随机博弈的非合作理性综合问题 So Koide、Yoshiaki Takata、Hiroyuki Seki IEICE 信息与系统汇刊，E107-D 卷，第 3 期，第 301-311 页 2024
Mu 微积分的子类，其冻结量词相当于配准自动机 高田义明、大西彰、仙田龙马、关宏之 IEICE 信息与系统汇刊，E106-D 卷，第 3 期，第 294-302 页 2023
用寄存器为计算模型表达的语言抽取引理 Rindo Nakanishi、Yoshiaki Takata、Hiroyuki Seki IEICE 信息与系统汇刊，E106-D 卷，第 3 期，第 284-293 页 2023
LTL 模型检查中将具有新鲜度属性的寄存器下推系统简化为下推系统 高田义明、仙田龙马、关宏之 IEICE 信息与系统汇刊，E105-D 卷，第 9 期，第 1620-1623 页 2022
寄存器上下文无关语法和相关形式的复杂性结果 仙田龙马、高田义明、关宏之 理论计算机科学，第 923 卷，第 99-125 页 2022
寄存器下推系统的 LTL 模型检查 仙田龙马、高田义明、关宏之 IEICE 信息与系统汇刊，E104-D 卷，第 12 期，第 2131-2144 页 2021
研究使用非易失性内存的 Java 对象持久化的开销 松本幸太郎、高田芳郎、宇川志代 计算机软件，第 38 卷，第 2 期，第 14-19 页 2021
寄存器下推系统的前向正则性保持特性 仙田龙马、高田义明、关宏之 IEICE 信息与系统汇刊，E104-D 卷，第 3 期，第 370-380 页 2021
加权寄存器自动机的最优运行问题 关弘之、吉村丽雄、高田义明 理论计算机科学，第 850 卷，第 185-201 页 2021
广义寄存器上下文无关语法 仙田龙马、高田义明、关宏之 IEICE 信息与系统汇刊，E103-D 卷，第 3 期，第 540-548 页 2020
基于扩展加权下推系统的基于信息的访问控制子集的形式化验证 拉米拉·阿尔瓦雷斯·巴勃罗，高田义明 IEICE 信息与系统汇刊，E97-D 卷，第 5 期，第 1149-1159 页 2014
根据信息流规范自动生成基于历史的访问控制 高田义明、关宏之 第八届验证和分析自动化技术国际研讨会 (ATVA 2010)，计算机科学讲义 6252，第 259-275 页 2010
信任协商中披露树策略的形式语言理论方法 高田义明、关宏之 IEICE 信息与系统汇刊，E92-D 卷，第 2 期，第 200-210 页 2009
基于语言的访问控制模型的表达能力比较 高田义明、关宏之 IEICE 信息与系统汇刊，E92-D 卷，第 5 期，第 1033-1036 页 2009
自组网络中信任建立的新证书链发现方法及其评估 毛里尚、安田郁也、高田义明、关宏之 日本信息处理学会交易，第 49 卷，第 1 期，第 362-374 页 2008
基于执行历史的访问控制的形式化模型和验证 高田芳郎、王静香、关宏之 IEICE Transactions D，第 J91-D 卷，第 4 期，第 847-858 页 2008
用于基于历史的切面编织的标记转换模型 A-LTS 及其表达能力 八木功、高田义明、关宏之 IEICE 信息与系统汇刊，E90-D 卷，第 5 期，第 799-807 页 2007
XML 文档的辅助功能指南一致性验证 高田芳郎、中村武、关宏之 IEICE Transactions D，第 J89-D 卷，第 4 期，第 705-715 页 2006
使用树自动机进行 XML 访问控制的静态分析 八木功、高田义明、关宏之、 计算机软件，第 23 卷，第 3 期，第 51-65 页 2006
HBAC：基于历史的访问控制模型及其模型检查 王静、高田义明、关宏之 第 11 届欧洲计算机安全研究研讨会 (ESORICS 2006)，计算机科学讲义 4189，第 263-278 页 2006

水平滑动即可查看表格的其余部分。

学术演讲、讲座等

  1. 广义均衡的非合作理性综合的计算复杂性，电子信息与通信工程师研究所软件科学研究组（2025）
  2. 没有分段信息的 3D Picross 和高度为 1 的 3D Picross 的 NP 完整性，日本信息处理学会第 36 届游戏信息学研究小组（2016）
  3. 第八届验证与分析自动化技术国际研讨会，（2010）
  4. 第十二届日本软件学会编程和编程语言研讨会，（2010 年）

科研基金

KAKEN 是由国家信息研究所提供的一项服务。

分类 研究主题 研究类别 研究期 作业编号
代表 多线程递归程序自动验证的形式化模型 年轻研究员(B) 2009 - 2010 21700045
代表 Actor模型型多线程递归程序的模型检查方法开发 基础研究（C） 2024 - 2026（计划） 24K14901
分享 图博弈中基于合理性的验证与自动合成的统一求解方法研究 基础研究（C） 2025 - 2028 年（计划） 25K15055

水平滑动即可查看表格的其余部分。

社会贡献和公共关系活动

外部委员会成员、学术活动等

  1. 日本信息处理学会四国分会分会委员（2024-2026）
  2. IEICE IEICE 软件科学研究委员会副主席（2024-2026）
  3. IEICE、IEICE四国分会委员（2024-2026）

一般讲座等

  1. 什么是程序？ ,

水平滑动即可查看表格的其余部分。