定理证明与VST验证工具

报告摘要: 交互式定理证明技术是验证程序复杂性质的重要手段，其主要思想是在现有自动化验证工具无力完成验证工作的情况下，由人提供额外信息从而辅助验证工具『理解』程序并验证其功能以及安全性。本报告将介绍 Verified Software Toolchain（VST）工具，该工具以交互式定理证明技术为基础，集成了学术界在程序逻辑等诸多方面的理论研究前沿成果，可用于验证复杂 C 语言程序的功能正确性与安全性，排查空指针引用漏洞、缓冲区溢出错误、并发数据访问竞争等各种问题。

报告人简介: 曹钦翔本科毕业于北京大学，博士毕业于美国普林斯顿大学，2018年回国任教。现为上海交通大学约翰霍普克洛夫特计算机科学中心副教授、博导，CCF形式化专委会委员。曹钦翔长期从事基于交互式定理证明的程序验证研究，著有Software Foundations系列教材第五卷Verifiable C。