顶会顶刊论坛

NASAC/FMAC

论坛主要包括最近一年发表在形式化和软件工程领域的顶级国际会议及顶级期刊上的代表性论文。

论坛组织委员会：

刘 辉（北京理工大学）

王俊杰（中国科学院软件研究所）

赵 亮（西安电子科技大学）

论坛主持人：

于 斌（西安电子科技大学）

王俊杰（中国科学院软件研究所）

日程安排：

时 间：2020年11月20日（星期五）09:00-12:30

2020年11月20日（星期五）14:00-17:00

地 点：重庆富力假日酒店 宴会厅3

论坛议程：

报告及嘉宾简介：

1. 甘庭：Nonlinear Craig Interpolant Generation (CAV 2020)

摘要：Craig interpolant generation for non-linear theory and its combination with other theories are still in infancy, although interpolation-based techniques have become popular in the verification of programs and hybrid systems where non-linear expressions are very common. In this paper, we first prove that a polynomial interpolant of the form h(x)>0 exists for two mutually contradictory polynomial formulas Φ(x,y) and ψ(x,z) , with the form f₁≥0∧⋯∧f_n≥0, where f_i are polynomials in x,y or x,z, and the quadratic module generated by f_i is Archimedean. Then, we show that synthesizing such interpolant can be reduced to solving a semi-definite programming problem (SDP). In addition, we propose a verification approach to assure the validity of the synthesized interpolant and consequently avoid the unsoundness caused by numerical error in SDP solving. Besides, we discuss how to generalize our approach to general semi-algebraic formulas. Finally, as an application, we demonstrate how to apply our approach to invariant generation in program verification.

简介：甘庭，武汉大学计算机学院讲师。2011年毕业于北京航空航天大学数学科学学院获得理学学士学位，2017年毕业于北京大学数学科学学院获得理学博士学位。中国计算机学会形式化方法专业委员会委员。主要从事程序验证、混成系统验证、自动推理、约束求解研究，在CAV，IJCAR，AAAI，IEEE TAC，JSC，CSIS，软件学报等国内外权威会议和期刊发表论文近10余篇。

2. 朱惠彪：Theoretical and Practical Aspects of Linking Operational and Algebraic Semantics for MDESL (TOSEM 2019)

摘要：Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. It contains interesting features such as event-driven computation and shared-variable concurrency. This article considers how the algebraic semantics links with the operational semantics for MDESL. Our approach is from both the theoretical and practical aspects. The link is proceeded by deriving the operational semantics from the algebraic semantics. First, we present the algebraic semantics for MDESL. We introduce the concept of head normal form. Second, we present the strategy of deriving operational semantics from algebraic semantics. We also investigate the soundness and completeness of the derived operational semantics with respect to the derivation strategy. Our theoretical approach is complemented by a practical one, and we use the theorem proof assistant Coq to formalize the algebraic laws and the derived operational semantics. Meanwhile, the soundness and completeness of the derived operational semantics is also verified via the mechanical approach in Coq. Our approach is a novel way to formalize and verify the correctness and equivalence of different semantics for MDESL in both a theoretical approach and a practical approach.

简介：朱惠彪，华东师范大学软件工程学院教授，博士生导师，教育部软件工程专业教学指导委员会委员。研究方向为高可信计算、形式化方法和信息物理融合系统，曾主持自然科学基金委中丹国际合作项目“信息物理融合系统的基础研究”（2011-2013）并且获得滚动资助（2014-2016）。“基于模型的可信软件理论与开发方法”获得2011年度教育部高等学校自然科学一等奖（第二完成人），分别于2013年和2017年获得高等教育上海市教学成果奖特等奖和一等奖（排名第二和第五），于2018年9月获得国家教学成果奖二等奖（排名第五）。

3. 王文胜：Making Streett Determinization Tight (LICS 2020)

摘要：Optimal determinization construction of Streett automata is an important research problem because it is indispensable in numerous applications such as decision problems for tree temporal logics, logic games and system synthesis. This paper presents a transformation from nondeterministic Streett automata (NSA) with n states and k Streett pairs to equivalent deterministic Rabin transition automata (DRTA) with n⁵ⁿ(n!)ⁿ states, O(n^{n^2} ) Rabin pairs for k = ω(n) and n⁵ⁿk^nk states, O(k^nk) Rabin pairs for k = O(n). This improves the state of the art Streett determinization construction with n⁵ⁿ(n!)ⁿ⁺¹ states, O(n²) Rabin pairs and n⁵ⁿk^nkn! states, O(nk) Rabin pairs, respectively. Moreover, deterministic parity transition automata (DPTA) are obtained with 3(n(n + 1) − 1)!(n!)ⁿ⁺¹ states, 2n(n+1) priorities for k = ω(n) and 3(n(k+1)−1)!n!k^nk states, 2n(k + 1) priorities for k = O(n), which improves the best construction with nⁿ(k + 1)^n(k+1)(n(k + 1) − 1)! states, 2n(k + 1) priorities. Further, we prove a lower bound state complexity for determinization construction from NSA to deterministic Rabin (transition) automata i.e. n⁵ⁿ(n!)ⁿ for k = ω(n) and n⁵ⁿk^nk for k = O(n), which matches the state complexity of the proposed determinization construction. Besides, we put forward a lower bound state complexity for determinization construction from NSA to deterministic parity (transition) automata i.e. 2^{Ω(n^2 log n)} for k = ω(n) and 2^{Ω(nk log nk)} for k = O(n), which is the same as the state complexity of the proposed determinization construction in the exponent.

简介：王文胜，西安电子科技大学16级计算机软件与理论专业博士研究生，师从田聪教授。本科毕业于西安电子科技大学信息与计算科学专业。研究兴趣包括自动机理论、时序逻辑、形式化验证。目前主要的研究方向为Omega自动机的确定化与求补，相关工作发表于理论计算机科学顶级会议LICS 2020，是今年该会议接收的唯一一篇由国内单位独立完成的论文。

4. 蔡少伟：Extended Conjunctive Normal Form and an Efficient Algorithm for Cardinality Constraints (IJCAI 2020)

摘要：Satisfiability (SAT) and Maximum Satisfiability (MaxSAT) are two basic and important constraint problems with many important applications. SAT and MaxSAT are expressed in CNF, which is difficult to deal with pseudo Boolean constraints (equally 0-1 integer programming). We introduce an extension of Conjunctive Normal Form, which expresses such constraints straightforward and does not need auxiliary variables or clauses. Then, we show how to transfer the techniques in SAT/MaxSAT under CNF to this extension, and develop a local search algorithm and a generalized Unit Propagation (UP) based algorithm. Experimental results on several real world problems show that our method has much better performance than state of the art MaxSAT, SAT, Pseudo-Boolean and ILP solvers, which indicates the power of the new formulation.

简介：蔡少伟，中科院软件所研究员、博士生导师、中科院青促会信息与管理分会会长、智源青年科学家。2012年于北京大学获计算机博士学位。他主要研究约束求解，组合优化和启发式算法。发表论文70余篇，包括CCF A类论文40余篇，多次获得国际SAT比赛金牌。提出的格局检测方法已经成为局部搜索算法的常用技术。他的成果在多个企业包括华为、腾讯、建设银行、微软等得到应用。担任IJCAI和AAAI会议SPC，并共同发起了IJCAI workshop “Heuristic search in Industry”

5. 刘咏梅：A Modal Logic for Joint Abilities under Strategy Commitments (IJCAI 2020)

摘要：Representation and reasoning about strategic abilities has been an active research area in AI and multi-agent systems. Many variations and extensions of alternating-time temporal logic ATL have been proposed. However, most of the logical frameworks ignore the issue of coordination within a coalition, and are unable to specify the internal structure of strategies. In this talk, I will introduce JAADL, a modal logic we recently proposed for joint abilities under strategy commitments, which is an extension of ATL. Firstly, we introduce an operator of elimination of (strictly) dominated strategies, with which we can represent joint abilities of coalitions. Secondly, our logic is based on linear dynamic logic (LDL), an extension of linear temporal logic (LTL), so that we can use regular expressions to represent commitments to structured strategies. I will present valid formulas in JAADL, give sufficient/necessary conditions for joint abilities, and show that model checking memoryless JAADL is in EXPTIME.

简介：刘咏梅，中山大学计算机科学系教授，博士生导师。于加拿大多伦多大学计算机科学系获博士学位。主要研究方向为人工智能中的知识表示与推理。研究工作涉及关于动作和变化的推理，关于知识和信念的推理，关于策略的推理，多智能模态逻辑中的遗忘，多智能体认知规划，智能体程序的自动验证和综合等。研究成果持续发表于国际人工智能会议IJCAI和AAAI上。

6. 张培歆：White-box fairness testing through adversarial sampling (ICSE 2020)

摘要：Although deep neural networks (DNNs) have demonstrated astonishing performance in many applications, there are still concerns on their dependability. One desirable property of DNN for applications with societal impact is fairness (i.e., non-discrimination). In this work, we propose a scalable approach for searching individual discriminatory instances of DNN. Compared with state-of-the-art methods, our approach only employs lightweight procedures like gradient computation and clustering, which makes it significantly more scalable than existing methods. Experimental results show that our approach explores the search space more effectively (9 times) and generates much more individual discriminatory instances (25 times) using much less time (half to 1/7).

简介：张培歆，2012年进入浙江大学学习，2016年保送浙江大学计算机科学与技术专业攻读硕士学位，2019年转为博士研究生，2019年至2020年在新加坡管理大学进行联合培养，师从王新宇教授与Jun Sun副教授。目前主要的研究方向为可信人工智能。其工作两获ACM SIGSOFT Distinguished Paper Award（ICSE 2018，ICSE 2020）。

7. 李念语：Scalable Multiple-View Analysis of Reactive Systems via Bidirectional Model Transformations (ASE 2020)

摘要：Systematic model-driven design and early validation enable engineers to verify that a reactive system does not violate its requirements before actually implementing it. Requirements may come from multiple stakeholders, who are often concerned with different facets-design typically involves different experts having different concerns and views of the system. Engineers start from a specification which may be sourced from some domain model, while validation is often done on state-transition structures that support model checking. Two computationally expensive steps may work against scalability: transformation from specification to state-transition structures, and model checking. We propose a technique that makes the former efficient and also makes the resulting transition systems small enough to be efficiently verified. The technique automatically projects the specification into submodels depending on a property sought to be evaluated, which captures some stakeholder’s viewpoint. The resulting reactive system submodel is then transformed into a state-transition structure and verified. The technique achieves cone-of-influence reduction, by slicing at the specification model level. Submodels are analysis-equivalent to the corresponding full model. If stakeholders propose a change to a submodel based on their own view, changes are automatically propagated to the specification model and other views affected. Automated reflection is achieved thanks to bidirectional model transformations, ensuring correctness. We cast our proposal in the context of graph-based reactive systems whose dynamics is described by rewriting rules. We demonstrate our view-based framework in practice on a case study within cyber-physical systems.

简介：李念语，北京大学16级博士研究生，正在攻读计算机软件与理论理学学位，师从北京大学金芝教授和焦文品教授。本科毕业于南京航空航天大学获软件工程工学学位，师从魏欧副教授。她的研究兴趣包括（人参与的）自适应系统、信息物理系统、形式化建模和验证，研究内容发表在JSS，PerCom，ASE，CogSci等期刊和会议上。她曾于2017.09-2018.03期间访问日本国立情报学研究所（NII，指导老师胡振江教授）且2019.09-2020.08期间访问卡耐基梅隆大学（CMU，指导老师David Garlan教授和Eunsuk Kang助理教授）。

8. 娄一翎：Can automated program repair refine fault localization? a unified debugging approach (ISSTA 2020)

摘要：A large body of research efforts have been dedicated to automated software debugging, including both automated fault localization and program repair. However, existing fault localization techniques have limited effectiveness on real-world software systems while even the most advanced program repair techniques can only fix a small ratio of real-world bugs. Although fault localization and program repair are inherently connected, their only existing connection in the literature is that program repair techniques usually use off-the-shelf fault localization techniques (e.g., Ochiai) to determine the potential candidate statements/elements for patching. In this work, we propose the unified debugging approach to unify the two areas in the other direction for the first time, i.e., can program repair in turn help with fault localization? In this way, we not only open a new dimension for more powerful fault localization, but also extend the application scope of program repair to all possible bugs (not only the bugs that can be directly automatically fixed). We have designed ProFL to leverage patch-execution results (from program repair) as the feedback information for fault localization. The experimental results on the widely used Defects4J benchmark show that the basic ProFL can already at least localize 37.61% more bugs within Top-1 than state-of-the-art spectrum and mutation based fault localization. Furthermore, ProFL can boost state-of-the-art fault localization via both unsupervised and supervised learning. Meanwhile, we have demonstrated ProFL's effectiveness under different settings and through a case study within Alipay, a popular online payment system with over 1 billion global users.

简介：娄一翎，2016年于北京大学计算机系获得学士学位，目前是北京大学计算机软件与理论方法方向的五年级博士生，导师为张路教授、郝丹副教授。她的研究方向主要围绕构建智能化的软件测试和调试系统，包括缺陷检测、定位与修复等。博士期间她已在ICSE、ISSTA、FSE、ASE等软件工程顶级会议和期刊上共发表论文十余篇，并获得ISSTA ACM SIGSOFT Distinguished Paper Award。

9. 潘敏学：Reinforcement Learning Based Curiosity-driven Testing of Android Applications (ISSTA 2020)

摘要：Mobile applications play an important role in our daily life, while it still remains a challenge to guarantee their correctness. Model-based and systematic approaches have been applied to Android GUI testing. However, they do not show significant advantages over random approaches because of limitations such as imprecise models and poor scalability. In this paper, we propose Q-testing, a reinforcement learning based approach which benefits from both random and model-based approaches to automated testing of Android applications. Q-testing explores the Android apps with a curiosity-driven strategy that utilizes a memory set to record part of previously visited states and guides the testing towards unfamiliar functionalities. A state comparison module, which is a neural network trained by plenty of collected samples, is novelly employed to divide different states at the granularity of functional scenarios. It can determine the reinforcement learning reward in Q-testing and help the curiosity-driven strategy explore different functionalities efficiently. We conduct experiments on 50 open-source applications where Q-testing outperforms the state-of-the-art and state-of-practice Android GUI testing tools in terms of code coverage and fault detection. So far, 22 of our reported faults have been confirmed, among which 7 have been fixed.

简介：潘敏学，南京大学副教授，CCF系统软件专委会委员。研究工作集中在软件建模与验证，软件分析与测试、智能软件工程等领域。主持有国家自然科学基金、江苏省自然科学基金，参与了国家重点研发计划、国家自然科学基金重大研究计划等多个科技项目；近期在TSE、ICSE、FSE、ISSTA、ASE、CAV等国际顶级期刊与会议上发表学术论文40余篇；获ISSTA2020杰出论文奖。

10. 任路遥：Detecting Numerical Bugs in Neural Network Architectures (FSE 2020)

摘要：Detecting bugs in deep learning software at the architecture level provides additional benefits that detecting bugs at the model level does not provide. This paper makes the first attempt to conduct static analysis for detecting numerical bugs at the architecture level. We propose a static analysis approach for detecting numerical bugs in neural architectures based on abstract interpretation. Our approach mainly comprises two kinds of abstraction techniques, i.e., one for tensors and one for numerical values. Moreover, to scale up while maintaining adequate detection precision, we propose two abstraction techniques: tensor partitioning and (elementwise) affine relation analysis to abstract tensors and numerical values, respectively. We realize the combination scheme of tensor partitioning and affine relation analysis (together with interval analysis) as DEBAR, and evaluate it on two datasets: neural architectures with known bugs (collected from existing studies) and real-world neural architectures. The evaluation results show that DEBAR outperforms other tensor and numerical abstraction techniques on accuracy without losing scalability. DEBAR successfully detects all known numerical bugs with no false positives within 1.7-2.3 seconds per architecture. On the real-world architectures, DEBAR reports 529 warnings within 2.6-135.4 seconds per architecture, where 299 warnings are true positives.

简介：任路遥，北京大学软件工程研究所一年级博士生，师从谢涛教授和熊英飞教授。曾前往卡内基梅隆大学和香港科技大学进行科研实习，也曾在微软中国和谷歌总部担任开发实习生。目前有多篇论文发表于包括ICSE、FSE、ASE、SANER在内的软件工程领域国际会议上，其中关于神经网络架构中数值缺陷的检测工作荣获了ACM杰出论文奖。

11． 刘忠鑫：Automating Just-In-Time Comment Updating (ASE 2020)

摘要：Code comments are valuable for program comprehension and software maintenance, and also require maintenance with code evolution. However, when changing code, developers sometimes neglect updating the related comments, bringing in inconsistent or obsolete comments (aka., bad comments). Such comments are detrimental since they may mislead developers and lead to future bugs. Therefore, it is necessary to fix and avoid bad comments. In this work, we argue that bad comments can be reduced and even avoided by automatically performing comment updates with code changes. We refer to this task as “Just-In-Time (JIT) Comment Updating” and propose an approach named CUP (Comment UPdater) to automate this task. CUP can be used to assist developers in updating comments during code changes and can consequently help avoid the introduction of bad comments. Specifically, CUP leverages a novel neural sequence-to-sequence model to learn comment update patterns from extant code-comment co-changes and can automatically generate a new comment based on its corresponding old comment and code change. Several customized enhancements, such as a special tokenizer and a novel co-attention mechanism, are introduced in CUP by us to handle the characteristics of this task. We build a dataset with over 108K comment-code co-change samples and evaluate CUP on it. The evaluation results show that CUP outperforms an information-retrieval-based and a rule-based baselines by substantial margins, and can reduce developers’ edits required for JIT comment updating. In addition, the comments generated by our approach are identical to those updated by developers in 1612 (16.7%) test samples, 7 times more than the best-performing baseline.

简介：刘忠鑫，浙江大学计算机科学与技术学院博士生，导师为李善平教授和夏鑫博士，主要研究方向为数据驱动的软件文档自动生成。目前已在TSE和ASE等国际学术期刊和会议发表了多篇论文。曾获得ASE 2018、2019和2020的ACM SIGSOFT Distinguished Paper Award。

12. 王俊杰：Context-aware In-process Crowdworker Recommendation (ICSE 2020)

摘要：Identifying and optimizing open participation is essential to the success of open software development. Existing studies highlighted the importance of worker recommendation for crowdtesting tasks in order to detect more bugs with fewer workers. However, these studies mainly focus on one-time recommendations with respect to the initial context at the beginning of a new task. This paper argues the need for in-process crowdtesting worker recommendation. We motivate this study through a pilot study, revealing the prevalence of long-sized non-yielding windows, i.e., no new bugs are revealed in consecutive test reports during the process of a crowdtesting task. This indicates the potential opportunity for accelerating crowdtesting by recommending appropriate workers in a dynamic manner, so that the non-yielding windows could be shortened.

To that end, this paper proposes a context-aware in-process crowdworker recommendation approach, iRec, to detect more bugs earlier and potentially shorten the non-yielding windows. It consists of three main components: 1) the modeling of dynamic testing context, 2) the learning-based ranking component, and 3) the diversity-based re-ranking component. The evaluation is conducted on 636 crowdtesting tasks from one of the largest crowdtesting platforms, and results show the potential of iRec in improving the cost-effectiveness of crowdtesting by saving the cost and shortening the testing process.

简介：王俊杰，中国科学院软件研究所副研究员，硕士生导师。主要从事软件数据挖掘、软件质量、智能化软件工程等方面的研究，近年来主要关注软件众包测试场景，研究如何提升众测质量、效率和效益，增强众测服务的智能化水平。主持和参与了多项国家自然科学基金项目、科技部重点研发计划等。在国际著名学术期刊/会议（如TSE、ICSE、FSE、ASE等）发表20余篇学术论文，荣获ICSE 2019、ICSE2020杰出论文奖。