本论坛的主要内容有两部分。一是召集国内程序设计语言研究的顶级年轻学者介绍最新的研究课题和成果, 互相交流,加强合作。二是讨论如何推进国内程序语言的研究和教育,缩短与国际上先进国家的差距,从本质 上解决软件中的卡脖子问题。
个人简介:北京大学讲席教授、北京大学信息科学技术学院副院长、计算机科学技术系主任。1996 年在日本东京大学信息工学专业获博士学位。曾担任东京大学情报理工学研究科教授,日本国立信息学研究所教授 / 系主任 , 北京大学长江讲座教授。长期从事程序设计语言和软件科学与工程的研究,在程序语言设计、结构化函数式程序设计、程序的自动综合和优化、并行程序设计、双向变换语言的设计和实现、以及软件的演化和维护等方面做出了 一系列开创性工作,曾获全日本最佳博士论文奖和日本软件科学会基础研究成就奖、日本工学会会士、欧洲科学院院士,IEEE Fellow、ACM 杰出科学家。
个人简介:南京大学教授、华为 2012 编程语言实验室主任。2007 年于耶鲁大学获博士学位,先后担任芝加哥丰田理工学院(TTIC)研究助理教授、中国科大教授和南京大学教授。主要研究方向为程序设计语言理论和形式化程序验证。提出并发程序模块化精化验证理论,并将其应用于细粒度并发算法、抢占式并发操作系统内核、以及编译器等核心系统软件的正确性和可靠性验证。在 POPL、PLDI、LICS、CAV、ACM TOPLAS 等国际会议和期刊上发表论文多篇,其中编译器验证工作获 PLDI'19优秀论文奖。担任 APLAS'15、APLAS'17 和 SETTA'17 的程序委员会主席 / 大会主席,多 次担任 POPL、PLDI、ESOP 等国际会议程序委员会委员。
报告摘要:计算机程序中的许多性质和常见错误(如除零错、数组越界、算术溢出、计算精度缺陷等),与程序中数值型变量及其上的数值运算密切相关。针对数值代码开展自动分析,检测数值相关错误,验证相关性质,修复相关缺陷,对于提高计算机软件(尤其是数值计算密集型安全攸关软件)的可信性具有重要意义。本报告将围绕程序中数值相关性质与错误,介绍基于抽象解释的数值程序分析与验证、基于数值近似的数值程序修复等方面的进展。
个人简介:2010 年于国防科技大学获工学博士学位。主要从事程序分析与验证、抽象解释相关研究。在ACM/IEEE Transactions、POPL、FSE 等期刊会议上录用发表论文多篇,出版教材译著 3 部。研究成果获省部级科技进步一等奖 1 项、二等奖 1 项。部分成果已在航天、国防等领域重大工程中应用。
报告摘要:概率程序语言作为用于描述和实现系统随机性的编程语言,在带有不确定性的场合中具有潜 在的应用价值。在一些要求苛刻的场合中,概率程序的关键性质必须得到保证,而形式化方法藉由其数 学上的严谨性,能够严格保障关键性质的正确性。本次演讲将围绕概率程序的终止性、代价分析、灵敏 性三个关键性质,阐述其形式化验证背后的数学理论和自动化验证算法。
个人简介:主攻形式化方法,在无穷状态系统、概率系统、一般命令式程序、概率程序等方面作出基 础性理论贡献。先后在国际知名学术会议和期刊上发表二十余篇学术论文,成果涵盖可判定性、计算 复杂性、算法以及数学理论等形式化方法各个基础理论层面。其中十余篇论文发表在 POPL、PLDI、 OOPSLA、CAV、ICALP(Track B)、TOPLAS、IandC 等国际著名学术会议及期刊上。获 2013 年度国际 学术会议 HSCC 最佳学生论文奖。指导学生获 2019 年度 IEEE 最佳学生论文奖(Lance Stafford Larson Prize)。
报告摘要:终止性是程序完全正确性的基本要求。终止性证明是程序验证最硬核的问题之一。目前已有 许多关于程序终止性的研究,然而所有这些研究都只面向单个程序版本。本工作主要考察演化场景下程 序的终止性证明,给出了首个针对该问题的解决方案。提出的方法能够广泛适应程序的各种演变,实现 终止性证据的有效复用。针对真实演化程序的实验验证了该方法的有效性。
个人简介:主要研究方向为形式化验证理论、方法及应用。在组合系统验证、演化系统验证、可满足 性判定理论、程序验证理论等方面取得成果。主持开发了模型检测工具 Beagle,软件验证工具 Ceagle 等工具,并成功的将上述工具应用于航空、航天、高铁等国家重大安全领域。在包括 POPL, CAV, PLDI, OOPSLA, ICSE, FSE, ASE, TOSEM, TSE, TC 等在内的国际重要会议和期刊上发表论文 60 余篇。 曾担任 CONCUR, FMCAD, APLAS, ICECCS, SETTA 等重要国际学术会议的程序委员会委员。
报告摘要:Conflict-Free Replicated Data Types (CRDTs) used in geographically distributed systems are designed with delicate conflict-resolution strategies to trade off strong consistency guarantees for availability and performance. People usually use strong eventual consistency (SEC) to specify the data consistency guarantee of CRDTs. However, it remains unclear how to characterize the functional correctness of CRDTs. This brings difficulties to modular verification of client programs using CRDTs. This talk presents a framework for verifying CRDTs and their clients. We first propose Abstract Converging Consistency (ACC), a new formulation of CRDTs' correctness. ACC specifies both data consistency and functional correctness. In particular, it supports abstract atomic specifications of CRDT operations, and establishes consistency between the concrete execution traces and the execution of the abstract atomic operations. Our Abstraction Theorem shows that ACC guarantees a contextual refinement between CRDT implementations and their atomic specifications. It allows us to soundly replace the concrete CRDTs with their abstractions when verifying client programs, thus enables modular and layered verification. We give a program logic to verify clients at the abstract level, and a proof method to verify concrete CRDT algorithms.
个人简介:主要研究并发程序验证理论,提出解决并发程序精化验证、终止性验证和功能正确性验 证等基础问题的新理论和新技术。在 POPL、PLDI、TOPLAS 等顶级会议和期刊上发表论文多篇。获 PLDI 2019 杰出论文奖。博士论文被评为 CCF 优博、中科院优博,被 MIT 评选为 2015 年度电子与计算 机领域"学术新星",获国家自然科学基金优秀青年基金支持。
报告摘要:交互式程序综合通过向用户提问明确程序编写的需求。为了降低用户负担,通过选择合适的问题来减少总共需要的问题数量非常重要。在本报告中,我将汇报我们对该问题的研究成果。具体而言,我们针对这个问题提出两个算法。SampleSy通过采样的方法模拟了一个决策树领域目前最好的选择策略,可以在较短的响应时间内选出所需的问题。EpsSy 通过引入少量错误率来进一步降低所需的总问题数。为了实现这两个算法,我们还设计了一个程序采样算法 VSampler,可以对概率版本空间代数所表达的程序分布进行采样。理论分析和实验表明,两个算法都很好的达到了设计的目标。
个人简介:研究兴趣是程序设计语言和软件工程,特别是程序分析、综合和修复。他提出了理论和方法降低程序编写和缺陷修复的代价。比如,基于差别的双向变换框架是最广泛使用的双向变换框架之一, ACS 将程序修复技术在公共数据集上的正确率从此前不到 40% 提升到 70% 以上。他的工作也被工业界采用,比如新一代 Linux 内核配置项目、燕云 DaaS 系统、华为公司等。他是 SATE18 的程序委员会联合主席,也在ICSE、FSE、ASE、ISSTA 等会议担任 PC。
报告摘要: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.
个人简介:研究领域为程序设计语言和软件工程,研究重点为编程系统和机器学习相关的交叉方向。一 方面,利用机器学习的思想来提高程序分析等编程系统的可用性,提出了逻辑与概率相结合的程序分析 等。另一方面,开发了新的程序分析和编程语言以提高机器学习系统的质量,在机器学习的可解释性、 公平性问题上都有所创新。工作发表在 PLDI、POPL、FSE、NeurIPS 等顶级会议上,并获 PLDI'14 和 FSE'15 杰出论文奖。曾担任 PLDI、SAS 等国际会议程序委员会委员。