自动验证复杂程序的功能正确性

报告摘要: QCP上海交通大学程序验证团队与合作者们共同研发的一款C 程序验证工具。其核心功能是要让用户可以验证并确认一个 C 语言能在所有允许的情况下都安全运行且行为符合预期。QCP 提供了专门的 IDE 套件，用户可以通过 VSCode 插件或者QCP 网页版使用。在 QCP 的 IDE 支持下，用户在编写程序的同时，可以随时查看当前程序状态所满足的断言（也就是符号执行的中间结果）， 不需要编写完整个函数即可进行验证，在编写过程中支持随时查看符号执行结果，第一时间检查断言标注的合理性， 修正其中的错误。QCP 2.0 Beta 版（https://www.qua.codes/）在之前的基础上，还提供了 AI 协作验证的支持，现在，许多中小规模的C程序功能正确性验证已经可以由QCP自动完成了。

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