CNCC｜领域特定语言碰撞安全编程：我们能否轻松写出没有Bug的程序？

熊英飞

北京大学 副教授

北京大学新体制长聘副教授，获2021年CCF-IEEE CS青年科学家奖。研究兴趣是程序合成、修复和分析。他提出理论和方法降低程序编写和缺陷修复的代价。比如，基于差别的双向变换框架是最广泛使用的双向变换框架之一，程序合成玲珑框架将程序修复的正确率从此前不到40%提升到80%以上。他的工作也被工业界采用，比如新一代Linux内核配置项目等。他获得2021年度CCF-IEEE CS青年科学家奖、MODELS十年最有影响力论文奖，5次获得ACM SIGSOFT/IEEE TCSE杰出论文奖。他在ICSE、FSE、PLDI、ASE、ISSTA等会议担任PC。

胡振江

北京大学 计算机学院院长/教授

1996年在日本东京大学获得博士学位。曾担任东京大学信息理工学研究科教授和日本国立信息学研究所教授/系主任。长期从事程序设计语言和软件科学与工程的研究，曾获全日本最佳博士论文奖、日本软件科学会基础研究成就奖，被评为21世纪先驱科学家（日本科学技术振兴机构）、日本工程院院士、日本工学会会士、欧洲科学院院士、IEEE会士、ACM杰出科学家。

报告题目：领域特定语言的敏捷开发及其支撑环境

在“软件定义一切”的信息时代，安全易用的领域特定语言越来越重要，但如何敏捷地开发面向领域专家使用的领域特定语言是一个未解决的重要问题。传统的嵌入式领域特定语言的设计方法导致领域特定语言与宿主语言的紧耦合，使得不熟悉宿主语言的领域专家很难使用。在这个报告中，我将简单地介绍北京大学程序语言实验室正在探索的支持领域特定语言敏捷开发的新方法及其支撑环境，包括一个可成长的结构化核心语言、一个基于语法糖的领域特定语言的定义方法、和一个支持领域特定语言的独立编辑、计算、运行的IDE环境的自动生成系统。

奚宏伟

波士顿大学 副教授

1998年从卡内基梅隆大学获得博士学位，奚博士主要关注采用先进类型理论指导现代程序语言设计。他设计了ATS程序设计语言，通过混合程序和证明的编程范式支持安全软件开发。他在用依赖类型和线性类型进行实用编程方面做过一系列先驱工作。他在ACM程序设计语言旗舰会议上担任PC（如POPL、PLDI和ICFP）。

报告题目：从函数式编程到线性函数式编程

ATS是一个基于Applied Type System框架的静态类型语言，同时支持依赖类型和线性类型。ATS核心是类似ML的函数式语言，支持数据类型、模式匹配、高阶函数等特性。尽管函数式语言可以显著简化程序构造和验证，但在资源利用率上存在浪费。比如，ML和Haskell的数据值都是在堆上分配的，只能通过垃圾回收释放。但是，在嵌入式实时系统中垃圾回收常常是不允许的。本报告将展现一种基于精化的方法，使得ATS的函数是程序可以被转换成线性函数式程序，从而可以在没有垃圾回收的情况实现类型安全的手动内存管理。基于此，ATS可以通过函数式语言直接支持低级嵌入式编程。

陈钢

南京航空航天大学 教授

CCF杰出会员。巴黎第七大学计算机系理论专业博士。研究兴趣：Lambda演算，领域专用语言，类型理论，高阶定理证明，函数式语言，EDA，形式化工程数学，飞行控制形式化数学，程序语言，硬件形式化验证，CPU自动生成，函数式硬件描述语言，PLC程序测试。在POPL，TCAD，IEEE on Nanotechnology等专业会议和杂志上发表多篇论文。开发多个软件原型产品：“C代码静态分析工具”，“PLC新型测试编程软件”，“工程科学编程软件”，“Verilog语法分析器”，“带类型云原生资源配置语言”。

报告题目：λ演算与基础软件

λ演算是现代计算机理论的基础。它直接促成了两个重要的研究方向：程序语言设计和高阶定理证明。函数式编程语言OCaml和高阶定理证明器Coq是这方面的两个代表性软件工具。在这两个工具之上正在形成一个具有颠覆性的新型软件和硬件开发方法。本次报告重点介绍南京航空航天大学形式化工程数学团队在领域专用语言、形式化验证、工业软件和EDA方面的研究工作。

曹钦翔

上海交通大学 副教授

本科毕业于北京大学，博士毕业于美国普林斯顿大学，2018年回国任教，现为上海交通大学约翰霍普克洛夫特计算机科学中心副教授。长期从事基于交互式定理证明的程序验证工具开发，并研究有关程序逻辑特别是分离逻辑的理论问题。是Verified Software Toolchain（VST）工具的主要开发者之一，首次实现了从业务逻辑，到源代码开发，再到编译的全链条正确性验证。

报告题目：从程序验证到安全编程

交互式定理证明技术是验证程序复杂性质的重要手段，其主要思想是在现有自动化验证工具无力完成验证工作的情况下，由人提供额外信息从而辅助验证工具『理解』程序并验证其功能以及安全性。经过探索，这一程序验证技术可以嵌入程序开发环境，从而实现『安全编程』。本报告将介绍 Verified Software Toolchain（VST）工具以及以此为基础的安全编程探索。该工具以交互式定理证明技术为基础，集成了学术界在程序逻辑等诸多方面的理论研究前沿成果，可用于验证复杂 C 语言程序的功能正确性与安全性，排查空指针引用漏洞、缓冲区溢出错误、并发数据访问竞争等各种问题。

沈嘉思

香港科技大学 助理教授（拟入职）

MIT的博士后，即将加入香港科技大学计算机科学及工程学系任助理教授。本科毕业于北京大学，硕士和博士毕业于MIT。研究兴趣是程序设计语言和软件工程。她在2020年被选中参加“EECS明日之星”研讨会。

报告题目：基于主动学习的软件再生

当前软件开发时间需要大量人力成本。我的研究的目标是自动化原来需要大量人工开销的工作，从而提升软件质量，降低开发代价。本报告将介绍一种新型的软件自动再生方法。给定一个已有程序，该方法将其作为黑盒学习，构建领域特定模型来捕获其功能，并采用该模型来生成新的程序。这个新的程序具有同样的核心功能，但经过一些潜在增强和变换，使得可以在不同的环境中正常运行。本报告将展现我们如何将该方法应用到不同领域并讨论在更广阔范围内该方法的潜在价值。