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

文章来源:  |  发布时间:2020-12-15  |  【打印】 【关闭

  

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

Speaker: 曹钦翔博士(John-Hopcroft中心,上海交通大学) 

Time: 202118(星期五)上午9:00 

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

    

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

    

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