[01-08] 基于定理证明的分离逻辑验证工具

Title: 基于定理证明的分离逻辑验证工具

Speaker: 曹钦翔博士（John-Hopcroft中心，上海交通大学）

Time: 2021年1月8日(星期五)上午10:00

Venue: 中科院软件园区5号楼334房间，计算机科学国家重点实验室报告厅

Abstract: 随着计算机软件在人们的生产生活中获得了广泛应用，一些软件安全问题逐步显现出来并受到重视，在过去的二十年中，基于交互式定理证明的功能正确性验证一步步从构想成为现实。其中，Verified Software Toolchain（VST）是用于利用定理证明器实现的用于验证C语言程序的安全性以及功能正确性的工具。本报告将介绍VST工具的框架、其提供的程序正确性保障以及其中的重要挑战。

Bio: 曹钦翔本科毕业于北京大学，2018年博士毕业于普林斯顿大学，现为上海交通大学约翰霍普克罗夫特计算机科学中心助理教授，博导。其长期从事基于交互式定理证明的程序验证研究，参与开发了 Verified Software Toolchain C程序验证工具，并参与撰写了 Software Foundation 系列教材第五卷。