[1]  本人主要研究方向为软件系统的形式化验证，包括形式化方法和证明框架的理论基础、设计和实现，以及应用该类框架验证关键性系统软件。目前主要研究内容包括：操作系统验证，编译器验证以及形式化验证理论及工具的开发

• [1]  2002.9～2006.7

  上海交通大学 - 电力系统及其自动化 - 工学学士 - 大学本科毕业 

• [2]  2006.9～2009.2

  上海交通大学 - 电力系统及其自动化 - 工学硕士 - 硕士研究生毕业 

• [3]  2009.9～2011.8

  康涅狄格大学 - 计算机软件与理论 - 理学硕士 - 硕士研究生毕业 

• [4]  2011.9～2016.12

  明尼苏达大学双城分校 - 计算机软件与理论 - 理学博士 - 博士研究生毕业 

• [1]  2020.3～至今

  上海交通大学电子信息与电气工程学院 | 长聘教轨副教授 

• [2]  2016.12～2019.12

  耶鲁大学计算机系 | 博士后