程序设计语言的研究与发展——如何推进国内程序设计语言的教育和研究？丨CNCC技术论坛

南京大学教授、华为2012编程语言实验室主任。2007年于耶鲁大学获博士学位，先后担任芝加哥丰田理工学院（TTIC）研究助理教授、中国科大教授和南京大学教授。主要研究方向为程序设计语言理论和形式化程序验证。提出并发程序模块化精化验证理论，并将其应用于细粒度并发算法、抢占式并发操作系统内核、以及编译器等核心系统软件的正确性和可靠性验证。在POPL、PLDI、LICS、CAV、ACM TOPLAS等国际会议和期刊上发表论文多篇，其中编译器验证工作获PLDI'19优秀论文奖。担任APLAS'15、APLAS'17和SETTA'17的程序委员会主席/大会主席，多次担任POPL、PLDI、ESOP等国际会议程序委员会委员。

报告二：概率程序的形式化方法理论

报告人简介：上海交通大学讲师，毕业于德国亚琛工业大学(RWTH Aachen)，主攻形式化方法，在无穷状态系统、概率系统、一般命令式程序、概率程序等方面作出基础性理论贡献。先后在国际知名学术会议和期刊上发表二十余篇学术论文，成果涵盖可判定性、计算复杂性、算法以及数学理论等形式化方法各个基础理论层面。其中十余篇论文发表在POPL、PLDI、OOPSLA、CAV、ICALP(Track B)、TOPLAS、IandC等国际著名学术会议及期刊上。获2013年度国际学术会议HSCC最佳学生论文奖。指导学生获2019年度IEEE最佳学生论文奖(Lance Stafford Larson Prize)

报告摘要：概率程序语言作为用于描述和实现系统随机性的编程语言，在带有不确定性的场合中具有潜在的应用价值。在一些要求苛刻的场合中，概率程序的关键性质必须得到保证，而形式化方法藉由其数学上的严谨性，能够严格保障关键性质的正确性。本次演讲将围绕概率程序的终止性、代价分析、灵敏性三个关键性质，阐述其形式化验证背后的数学理论和自动化验证算法。

报告三：演化程序的终止性证明

报告人简介：清华大学副教授。2008年毕业于清华大学计算机系，获工学博士学位。自2008年起于清华大学软件学院任教。主要研究方向为形式化验证理论、方法及应用。在组合系统验证、演化系统验证、可满足性判定理论、程序验证理论等方面取得成果。主持开发了模型检测工具Beagle，软件验证工具Ceagle等工具，并成功的将上述工具应用于航空、航天、高铁等国家重大安全领域。在包括POPL, CAV, PLDI, OOPSLA, ICSE, FSE, ASE, TOSEM, TSE, TC等在内的国际重要会议和期刊上发表论文60余篇。曾担任CONCUR, FMCAD, APLAS, ICECCS, SETTA等重要国际学术会议的程序委员会委员。

报告摘要：终止性是程序完全正确性的基本要求。终止性证明是程序验证最硬核的问题之一。目前已有许多关于程序终止性的研究，然而所有这些研究都只面向单个程序版本。本工作主要考察演化场景下程序的终止性证明，给出了首个针对该问题的解决方案。提出的方法能够广泛适应程序的各种演变，实现终止性证据的有效复用。针对真实演化程序的实验验证了该方法的有效性。

报告五：交互式程序综合中的问题选择

报告人简介：北京大学副教授。2009年从日本东京大学获得博士学位，2009-2011年在加拿大滑铁卢大学工作，2012年加入北京大学，现任新体制长聘副教授。熊英飞的研究兴趣是程序设计语言和软件工程，特别是程序分析、综合和修复。他提出了理论和方法降低程序编写和缺陷修复的代价。比如，基于差别的双向变换框架是最广泛使用的双向变换框架之一，ACS将程序修复技术在公共数据集上的正确率从此前不到40%提升到70%以上。他的工作也被工业界采用，比如新一代Linux内核配置项目、燕云DaaS系统、华为公司等。他是SATE18的程序委员会联合主席，也在ICSE、FSE、ASE、ISSTA等会议担任PC。

报告摘要：交互式程序综合通过向用户提问明确程序编写的需求。为了降低用户负担，通过选择合适的问题来减少总共需要的问题数量非常重要。在本报告中，我将汇报我们对该问题的研究成果。具体而言，我们针对这个问题提出两个算法。SampleSy通过采样的方法模拟了一个决策树领域目前最好的选择策略，可以在较短的响应时间内选出所需的问题。EpsSy通过引入少量错误率来进一步降低所需的总问题数。为了实现这两个算法，我们还设计了一个程序采样算法VSampler，可以对概率版本空间代数所表达的程序分布进行采样。理论分析和实验表明，两个算法都很好的达到了设计的目标。

报告六：Interpreting Neural Network Judgments via Minimal, Stable, and Symbolic Corrections

报告人简介：北京大学助理教授。2017年获美国佐治亚理工博士学位，2017-2020年于美国麻省理工学院担任博士后研究员。他的研究领域为程序设计语言和软件工程，研究重点为编程系统和机器学习相关的交叉方向。一方面，他利用机器学习的思想来提高程序分析等编程系统的可用性，提出了逻辑与概率相结合的程序分析等。另一方面，他开发了新的程序分析和编程语言以提高机器学习系统的质量，在机器学习的可解释性、公平性问题上都有所创新。他的工作曾发表在PLDI、POPL、FSE、NeurIPS等顶级会议上，并获PLDI'14和FSE'15杰出论文奖。

报告摘要：In this talk, I will demonstrate how to leverage ideas in programming languages to address one of the key problems in machine learning, interpretability. In particular, I will present a new algorithm to generate minimal, stable, and symbolic corrections to an input that will cause a neural network with ReLU activations to change its output. We argue that such a correction is a useful way to provide feedback to a user when the network’s output is different from a desired output. Our algorithm generates such a correction by solving a series of linear constraint satisfaction problems. The technique is evaluated on three neural network models: one predicting whether an applicant will pay a mortgage, one predicting whether a first-order theorem can be proved efficiently by a solver using certain heuristics, and the final one judging whether a drawing is an accurate rendition of a canonical drawing of a cat.