西南大学计信院前沿学术报告

Southwest University IT Faculty Seminar

报告题目：语言独立的程序验证和区块链验证

Language-Independent Program Verification and Blockchain Verification

时间：2018年 6 月 20日（星期三）下午14:30

地点： 25教一楼报告厅（25-0114）

报告人：陈霄泓（美国伊利诺伊大学香槟分校）

报告人简介：

?

陈霄泓是伊利诺伊大学香槟分校的计算机方向博士研究生，本科毕业于北京大学数学系，主要研究方向是程序语义，程序验证，和程序逻辑。其主要研究思想认为程序语言应有形式化语义定义，且所有语言相关的工具，包括程序验证器，都应由语言的语义自动机器生成。陈霄泓目前是形式化系统研究室（Formal Systems Laboratory）的一名研究员，参与和领导多个研究项目，包括基础理论和实际应用，其研究主要是关于语言独立的语义框架K。陈霄泓是《K语义》标准文档的合作者之一。（https://github.com/kframework/kore/blob/master/docs/semantics-of-k.pdf）

内容摘要：

程序验证研究一个程序是否满足其形式化描述。传统程序验证方法通常是基于某一类程序逻辑，结合一套证明规则，来定义语言的语义，分析研究程序的性质。经典的程序逻辑包括霍尔逻辑，动态逻辑，分离逻辑等。然而这些经典程序逻辑通常定义复杂，理解困难，无法直接执行，且容易出错。当语言更新迭代时，程序逻辑也要一并修改，代价高昂。因此，在实际应用，尤其是程序语言快速迭代的区块链语言和智能合约验证中，经典程序逻辑使用起来代价较高且使用不便。

本报告介绍一种新的程序验证的途径，称为语言独立或者语言无关的程序验证，基于形式化语言设计框架K（www.kframework.org）。本报告将展示如何利用语言的可执行语义，不借助其他任何直接或非直接的语义信息，通过一个语言无关的证明系统，来实现对任意语言、任意程序、任意性质的自动验证。报告将讨论基础理论和实际应用。理论方面，报告将简单介绍K框架的理论基础，匹配逻辑，并且展示许多重要的程序逻辑可以在匹配逻辑中定义。应用方面，报告将简要列举一些已经完成和正在进行的研究项目，包括区块链语言和智能合约验证等工作。