合作交流 / 学术报告

[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 系列教材第五卷。