100%的程序正确性保障——交互式程序正确性证明

Speaker:    Prof.Qinxiang Cao

Time:        10:30-11:30, Mar. 20

Location:    SIST 1A 200

Host:         Prof. Fu Song

Abstract:

随着软件技术的进步和软件行业的发展，计算机软件在人们的生产生活中获得了广泛应用，而这也使得一些软件安全问题逐步显现出来并受到重视。在过去的十年中，学界逐步提出并发展了基于交互式程序正确性证明的工具。其中，Verified Software Toolchain（VST）是用于证明C语言程序的安全性以及功能正确性的工具。本报告将介绍VST这一类工具的一般框架以及其提供的程序正确性保障.

Bio: 

曹钦翔，本科毕业于北京大学，博士毕业于美国普林斯顿大学，2018年回国任教，现为上海交通大学助理教授、博导。其长期从事基于交互式程序正确性证明工具的开发，并研究有关程序逻辑的理论问题。曹钦翔是Verified Software Toolchain（VST）在过去五年内的主要开发者之一，他最早提出将深层嵌入技术用于交互式程序正确性证明工具中程序逻辑的形式化。在理论研究方面，曹钦翔在2017统一了分离逻辑的语义学，在此之前，许多不同版本的分离逻辑语义被广泛认为是无法相互兼容的。

SIST-Seminar 18136