在访问期间主要在以下两个方面开展了研究：网络安全协议的形式化方法研究，主要利用进程代数理论和模型，开发了面向无线传感网安全协议的形式化验证新方法；基于云计算的形式化验证方法，主要利用云计算并行架构，研究设计基于云计算的模型检测方法和过程，重点研究突破系统状态的拆分和存储等关键问题。回国后，将计划通过申报省部级国际合作课题等，延续形式化方法在安全系统验证以及利用云计算提升形式化自动验证效率的研究方向，并带领浙工大的研究生团队逐步加入PAT研究小组，在软件形式化理论及其在软件安全中的应用方面开展国际前沿研究，有效提升我校的研究生学术创新能力。