出访团组名称

张杰等1人赴澳大利亚科研团组

出访人团组成员

部门

职务

张杰

信息科学与技术学院

副教授

出访国家或地区

澳大利亚

拟出访日期

2017.1.13-2017.1.28

邀请单位

新南威尔士大学

经费来源及

拟支出金额

经费来源：校内预研基金

拟支出金额：103605元

出访任务

及日程安排

2017年1月13日

乘飞机前往澳大利亚悉尼，当日抵达，入住新南威尔士。

2017年1月14日

拜访合作方教授，商谈访问期间的一些具体安排。与访问课题组其他成员讨论，准备讨论议题和内容。

2017年1月15日—2017年1月21日

到访合作学院和课题组，向合作教授及对方相关课题组简介形式化验证方法及高阶逻辑定理证明器HOL4，介绍我方的研究工作，并顺序听取对方课题组每一位相关人员的研究报告，与每位人员进行深入的讨论，共同探讨研究双方在大型软件上的形式化验证方法的可行性实现方案。

2017年1月22日—2017年1月28日

具体研究并分析SOC功能实现结构，寻找提取关键的功能模块；

根据模型检验和定理证明特点，进行验证模块分解、建模，同时参加课题组讨论会，研究基于软硬件的形式化验证在模块划分上的方法。

2017年1月29日—2017年2月4日

与合作教授进一步讨论有关算法的验证方法，研究如何使用高阶逻辑来表示遗传算法、蚁群算法等，并行进行建模和验证；查阅并阅读前沿文献，与课题组讨论通过推理和形式化验证为机器人建立可靠的操作系统，以及路径规划系统的可行性。参加课题组讨论会。

2017年2月5日—2017年2月11日

利用高阶逻辑具有较强表达能力的特点，以高阶逻辑定理证明器HOL4（High Order Logic-4）为工具，探讨在HOL4系统中引入遗传算法，并建立合理的高阶逻辑模型，同时参加课题组讨论会。

2017年2月12日—2017年2月18日

从研究机器人的运动规划出发，依据概率等方法，探讨基于HOL4系统构建能够为机器人控制系统所使用的运动规划算子库，最终提高机器人控制系统的可靠性和智能化；研究如何使用高阶逻辑来表示遗传算法、蚁群算法等，并行进行建模和验证；同时参加课题组讨论会。

2017年2月19日—2017年2月25日

整理研究材料， 写总结报告。做有关形式化验证的学术报告，并与合作方研究小组进行进一步的讨论。

2017年2月26日

与合作教授关于组合验证进行深入的探讨，制定可行的未来的合作研究目标和计划

2017年2月27日

从悉尼乘机返回北京。

2017年2月28日

抵达北京。

事后公示

请在回国后1个月内在单位内部公布上述公示内容的实际执行情况和出访报告。

公示期7天，如有异议，请于12月13日下午5:00前请将书面意见反馈至国际交流与合作处，联系电话：010-64448919。