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

文章来源:  |  发布时间:2021-09-25  |  【打印】 【关闭

  
  

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

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

  Time: 2021-09-25(星期五)上午9:00

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

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

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

百度