副教授，上海市浦江人才，长期研究程序验证、程序逻辑与交互式定理证明，并研究人工智能技术在这些领域的应用。他2013年本科毕业于北京大学获得哲学（逻辑与科学哲学）学士学位获得数学双学士学位，于2018年在美国普林斯顿大学获得计算机博士学位。他在程序验证领域的代表性研究成果VST、VST-A验证工具是目前用于验证实际程序功能正确性的最好结果之一，相关成果发表于POPL、OOPSLA、JAR等国际一流会议与期刊。2016年的哥德尔奖得主Peter O'Hearn曾评价这些工作“在具有挑战性的程序验证问题中获得了令人印象深刻的成果”。他参与发起了TPChina定理证明开放社区，他目前是中国计算机学会形式化方法专委会的执行委员。