2024-12-31
2025年2月28日，上海期智研究院第12期“SQZ Talk”学术论坛邀请上海交通大学副教授曹钦翔带来专题报告“Formal Verification of OS Kernel's Functional Correctness”。论坛由研究院PI袁洋教授主持。
报告人简介
曹钦翔
上海期智研究院兼职研究员
上海交通大学副教授
曹钦翔，上海市浦江人才，长期研究程序验证、程序逻辑与交互式定理证明，并研究人工智能技术在这些领域的应用。他2013年本科毕业于北京大学获得哲学（逻辑与科学哲学）学士学位获得数学双学士学位，于2018年在美国普林斯顿大学获得计算机博士学位。他在程序验证领域的代表性研究成果VST、VST-A验证工具是目前用于验证实际程序功能正确性的最好结果之一，相关成果发表于POPL、OOPSLA、JAR等国际一流会议与期刊。2016年的哥德尔奖得主Peter O'Hearn曾评价这些工作“在具有挑战性的程序验证问题中获得了令人印象深刻的成果”。他参与发起了TPChina定理证明开放社区，他目前是中国计算机学会形式化方法专委会的执行委员。
专题报告
自2022年以来，曹钦翔教授与中科院软件所、北京大学等单位合作，使用交互式定理证明方法与其带领上海交通大学团队研发的Quanlified C Programming（QCP）验证工具，合作开展了若干项操作系统内核的形式化验证工作。本次报告介绍了交互式定理证明与程序验证的发展现状，并分享在这些操作系统验证实践与验证工具开发过程中的一些经验。
报告结束后，科研人员们讨论了程序形式化验证中硬件与编译器的基础假设问题、编译器的数学描述以及霍尔逻辑在程序验证中的核心作用。此外，还探讨了程序验证的可信基问题，特别是如何通过定理证明器内核设计与程序验证工具的验证机制设计做到在提升自动化程度的同时保证可靠性。
袁洋 SQZ PI
沈马成 SQZ PI
刘畅 SQZ高级研究员
何弈拓 SQZ研究员
