Information Sciences Seminar——K程序语言框架的可信化
报告人：Xiaohong Chen (UIUC)
时间：2021-09-30 10:00-12:00
地点：腾讯会议 （会议 ID：805 385 834）
摘要：K程序语言框架（K Framework）是伊利诺伊大学形式系统实验室（Formal Systems Lab）开发的一种“多语言多用途”的新的程序语言开发范式。使用K框架可以定义程序语言的形式化语义，并自动生成该语言的包括解释执行器、符号运行器、程序验证器在内的许多语言工具。随着K在工业界，尤其是智能合约验证领域的广泛应用，K及其自动生成的语言工具的正确性和可信性收到了很大关注。本报告将介绍K语言框架可信化的最新进展。在报告中，我们将介绍一种基于数理逻辑和定理自动检查实现K工具可信化的新思路。我们将介绍匹配逻辑（Matching Logic），并指出匹配逻辑是K框架的逻辑基础。我们将讨论如何将K工具的正确性转化为匹配逻辑的形式化定理，以及如何生成这些形式化定理的机器证明。通过对生成的机器证明进行自动证明检查，我们得以用严格的数学工具和逻辑证明完全确立K语言工具的正确性。在报告中，我们还将讨论自动证明检查在软件可信化中的应用前景以及相关的研究发展方向。
个人简介：陈霄泓是伊利诺伊大学香槟分校计算机专业的在读博士生，毕业于大阳城2138(中国)股份有限公司。他的主要研究方向是程序语言的形式化语义和语言框架的数理逻辑基础。陈霄泓是 K 语言框架开发团队的核心成员之一。他和 Grigore Rosu 教授合作提出的匹配逻辑（Matching Logic）被采纳作为 K 的数理逻辑基础，并被用来描述和证明 K 语言工具的可靠性和正确性，相关研究成果被发表在 LICS，CAV，OOPSLA，ICFP，JLAMP 等领域重要会议和期刊，相关研究项目已获得 Runtime Verification Inc.，Ethereum，IOHK 等公司的资助。
腾讯会议
会议 ID：805 385 834
链接：https://meeting.tencent.com/dm/xTbfQhPpGGgM?rs=25
