曹钦翔(1990-),男,博士,上海交通大学副教授,博士生导师,CCF专业会员,形式化专委会执行委员.长期从事基于定理证明的程序验证与程序逻辑研究,参与开发了VST (Verified Software Toolchain)验证工具,并参与撰写了Coq定理证明知名教材《Software Foundations》的第5卷;詹博华(1989-),男,博士,中国科学院软件研究所副研究员,CCF专业会员,形式化专委会执行委员.主要研究方向是交互式定理证明,关注证明自动化方法和工具设计,以及嵌入式系统的建模和验证.在Isabelle定理证明器中开发了auto2证明自动化工具,应用于基于集合论的形式化数学和基于分离逻辑的程序验证.此外,参与开发了量子程序验证工具QHLProver.目前正在开发HolPy交互式定理证明器;赵永望(1979-),男,博士,浙江大学教授,博士生导师,移动终端安全浙江省工程实验室主任,工信部重大专项首席科学家,CCF杰出会员.担任ARINC 653国际操作系统标准委员会委员、CCF系统软件专委会和形式化方法专委会执行委员、国际标准化组织ISO/IEC JTC1 SOA研究组组长等.主要研究方向包括形式逻辑与验证、操作系统安全、编程语言原理等;主持和参与国家自然基金重点项目、工信部重大专项、载人航天工程重点项目等20余项,2011年和2017年分别获得中国电子学会和山东省科技进步一等奖

赵永望,E-mail:zhaoyw@zju.edu.cn