Title: 基于定理證明的分離邏輯驗證工具

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

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

　　Venue: 中科院軟件園區5號樓334房間，計算機科學國家重點實驗室報告廳

　　Abstract: 隨著計算機軟件在人們的生產生活中獲得了廣泛應用，一些軟件安全問題逐步顯現出來并受到重視，在過去的二十年中，基于交互式定理證明的功能正確性驗證一步步從構想成為現實。其中，Verified Software Toolchain（VST）是用于利用定理證明器實現的用于驗證C語言程序的安全性以及功能正確性的工具。本報告將介紹VST工具的框架、其提供的程序正確性保障以及其中的重要挑戰。

　　Bio: 曹欽翔本科畢業于北京大學，2018年博士畢業于普林斯頓大學，現為上海交通大學約翰霍普克羅夫特計算機科學中心助理教授，博導。其長期從事基于交互式理證明的程序驗證研究，參與開發了 Verified Software Toolchain C程序驗證工具，并參與撰寫了Software Foundation 系列教材第五卷。