报告题目：Foundationally Sound Program Verification Tools
报告人：   曹钦翔 博士 （上海交通大学）
主持人：   邓玉欣 教授
报告时间：10月11日  周四10:00 - 11:00
报告地点：理科大楼1002室

报告摘要：
Computer scientists have gained great success in developing foundationally sound program verification systems in the past decade. The word foundationally means: not only program correctness properties are verified, but the correctness proofs and the depended proof rules are also verified and machine-checked. In this talk, I will introduce new techniques used in Verified Software Toolchain (a.k.a. VST, a foundationally sound C program verification tool) and discuss the future of interactive program verification.

报告人简介：
Qinxiang Cao is an assistant professor of Shanghai Jiao Tong University. He was a logic-major bachelor student of Peking University (2009~2013) and he was a Ph.D student of Princeton University (2013~2018). His research includes a series of program-logic-related topics: interactive theorem proving, Hoare logic for concurrent programs, program verification for randomized programs etc. In 2017, he unifies all different semantics of separation logics, some of which were thought to be incompatible with each other for a long time.