Deliberation is a common and natural behavior in human daily life. For example, when writing papers or articles, we usually first write drafts, and then iteratively polish them until satisfied. In light of such a human cognitive process, we propose DECOM, which is a multi-pass deliberation framework for automatic comment generation. DECOM consists of multiple Deliberation Models and one Evaluation Model. Given a code snippet, we first extract keywords from the code and retrieve a similar code fragment from a pre-defined corpus. Then, we treat the comment of the retrieved code as the initial draft and input it with the code and keywords into DECOM to start the iterative deliberation process. At each deliberation, the deliberation model polishes the draft and generates a new comment. The evaluation model measures the quality of the newly generated comment to determine whether to end the iterative process or not. When the iterative process is terminated, the best-generated comment will be selected as the target comment. Our approach is evaluated on two real-world datasets in Java (87K) and Python (108K), and experiment results show that our approach outperforms the state-of-the-art baselines. A human evaluation study also confirms the comments generated by DECOM tend to be more readable, informative, and useful.

Fangwen Mu

Institute of Software Chinese Academy of Sciences

Xiao Chen

Institute of Software Chinese Academy of Sciences

Lin Shi

ISCAS

China

Song Wang

York University

Canada

Qing Wang

Institute of Software at Chinese Academy of Sciences

China

Recommender systems (RSs) are increasingly being used to help in all sorts of software engineering tasks, including modelling. However, building a RS for a modelling notation is costly. This is especially detrimental for development paradigms that rely on domain-specific languages (DSLs), like model-driven engineering and lowcode approaches. To alleviate this problem, we propose a DSL called Droid that facilitates the configuration and creation of RSs for particular modelling notations. Its tooling provides automation for all phases in the development of a RS: data preprocessing, system configuration for the modelling language, evaluation and selection of the best recommendation algorithm, and deployment of the RS into a modelling tool. A video of the tool is available at https://www.youtube.com/watch?v=VHiObfKUhS0.

Lissette Almonte

Universidad Autónoma de Madrid

Spain

Esther Guerra

Universidad Autónoma de Madrid

Iván Cantador

Universidad Autónoma de Madrid

Spain

Juan de Lara

Autonomous University of Madrid

Spain

We present RoboSimVer, a tool for modeling and analyzing RoboSim Models. It uses a graphical modeling approach to model platform-independent simulation models of Robotics called RoboSim. For model analysis, we implemented a model-transformation approach to translate RoboSim models into NTA (Network of Timed Automata) and its stochastic version SHA (Stochastic Hybrid Automata) based on some patterns and mapping rules. RoboSimVer is able to get a simulation model. It also provides different rigorous verification techniques to check whether the simulation models satisfy property constraints. For experimental demonstrations, we adopt the case study Alpha algorithm for robotics. We use a robotic platform model of swarm robots in an uncertain environment, to illustrate how our tool supports the verification of stochastic and hybrid systems. The demonstration video of the tool is available at https://youtu.be/mNe4q64GkmQ

Dehui Du

East China Normal University

Ana Cavalcanti

University of York

United Kingdom

JihuiNie

East China Normal University

The robustness of deep neural networks is crucial to modern AI-enabled systems. Formal verification has been demonstrated effective in providing certified robustness guarantees. Sigmoid-like neural networks have been adopted in a wide range of applications. Due to their non-linearity, Sigmoid-like activation functions are usually over-approximated for efficient verification, which inevitably introduces imprecision. Considerable efforts have been devoted to finding the so-called tighter approximations to obtain more precise verification results. However, existing tightness definitions are heuristic and lack a theoretical foundation. We conduct a thorough empirical analysis of existing neuron-wise characterizations of tightness and reveal that they are superior only on specific neural networks. We then introduce the notion of network-wise tightness as a unified tightness definition and show that computing network-wise tightness is a complex non-convex optimization problem. We bypass the complexity from different perspectives via two efficient, provably tightest approximations. The experimental results demonstrate the promising performance achievement of our approaches over state of the art: (i) achieving up to 436.36% improvement to certified lower robustness bounds; and (ii) exhibiting notably more precise verification results on convolutional networks.

Zhaodi Zhang

East China Normal University

Yiting Wu

East China Normal University

Si Liu

ETH Zurich

Switzerland

Jing Liu

East China Normal University

Min Zhang

East China Normal University

China

Modern programs are usually heap-based, where the programs manipulate heap-based data structures to perform computations. In software engineering tasks such as test generation and bounded verification, we need to determine the existence of a reachable heap state that satisfies a given specification, or construct the heap state by a sequence of calls to the public methods. Given the huge space combined from the methods and their arguments, the existing approaches typically adopt static analysis or heuristic search to explore only a small part of search space in the hope of finding the target state and target call sequence early on. However, these approaches do not have satisfactory performance on many real-world complex methods and specifications. In this paper, we propose an efficient synthesis algorithm for method call sequences, including an offline procedure for exploring all reachable heap states within a scope, and an online procedure for generating a method call sequence from the explored heap states to satisfy the given specification. To improve the efficiency of state exploration, we introduce a notion of abstract heap state for compactly representing heap states of the same structure and propose a strategy of merging structurally-isomorphic states. The experimental results demonstrate that our approach substantially outperforms the baselines in both test generation and bounded verification.

Yunfan Zhang

Peking University

China

Ruidong Zhu

Peking University

Yingfei Xiong

Peking University

China

Tao Xie

Peking University

China

Abstract—Over the past few years, SMT string solvers have found their applications in an increasing number of domains, such as program analyses in mobile and Web applications, which require the ability to reason about string values. A series of research has been carried out to find quality issues of string solvers in terms of its correctness and performance. Yet, none of them has considered the performance regressions happening across multiple versions of a string solver. To fill this gap, in this paper, we focus on solver performance regressions (SPRs), i.e., unintended slowdowns introduced during the evolution of string solvers. To this end, we develop SPRFinder to not only generate test cases demonstrating SPRs, but also localize the probable causes of them, in terms of commits. We evaluated the effectiveness of SPRFinder on three state-of-the-art string solvers, i.e., Z3Seq, Z3Str3, and CVC4. The results demonstrate that SPRFinder is effective in generating SPR-inducing test cases and also able to accurately locate the responsible commits. Specifically, the average running time on the target versions is 13.2× slower than that of the reference versions. Besides, we also conducted the first empirical study to peek into the characteristics of SPRs, including the impact of random seed configuration for SPR detection, understanding the root causes of SPRs, and characterizing the regression test cases through case studies. Finally, we highlight that 149 unique SPR-inducing commits were discovered in total by SPRFinder, and 16 of them have been confirmed by the corresponding developers. The original paper can be accessed from https://ieeexplore.ieee.org/abstract/document/9760153

Yao Zhang

Xiaofei Xie

Singapore Management University, Singapore

Singapore

Yi Li

Nanyang Technological University, Singapore

Singapore

Yun Lin

National University of Singapore

Singapore

Sen Chen

Tianjin University

China

Yang Liu

Nanyang Technological University

Xiaohong Li

TianJin University

China

Code clone detection aims to find functionally similar code fragments, which is becoming more and more important in the field of software engineering. Many code clone detection methods have been proposed, among which tree-based methods are able to handle semantic code clones. However, these methods are difficult to scale to big code due to the complexity of tree structures. In this paper, we design \emph{Amain}, a scalable tree-based semantic code clone detector by building Markov chains models. Specifically, we propose a novel method to transform the complex original tree into simple Markov chains and compute the similarity of all states in these chains. After obtaining all similarity scores, we feed them into a machine learning classifier to train a code clone detector. To examine the effectiveness of \emph{Amain}, we evaluate it on two widely used datasets namely Google Code Jam and BigCloneBench. Experimental results show that \emph{Amain} is superior to five state-of-the-art code clone detection tools (\ie \emph{SourcererCC}, \emph{Deckard}, \emph{RtvNN}, \emph{ASTNN}, and \emph{SCDetector}). Furthermore, compared to a recent tree-based code clone detector \emph{ASTNN}, \emph{Amain} is more than 160 times faster in predicting semantic code clones.

Yueming Wu

Nanyang Technological University

Siyue Feng

Huazhong University of Science and Technology

Deqing Zou

Huazhong University of Science and Technology

Hai Jin

Huazhong University of Science and Technology

China