Precise pointer analysis is desired since it is a core technique to find memory defects. There are several dimensions of pointer analysis precision, flow sensitivity, context sensitivity, field sensitivity and path sensitivity. For static analysis tools utilizing pointer analysis, considering all dimensions is difficult because the trade-off between precision and efficiency should be balanced. This paper presents TsmartGP, a static analysis tool for finding memory defects in C programs with a precise and efficient pointer analysis. The pointer analysis algorithm is flow, context, field, and quasi path sensitive. Control flow automatons are the key structures for our analysis to be flow sensitive. Function summaries are applied to get context information and elements of aggregate structures are handled to improve precision. Path conditions are used to filter unreachable paths. For efficiency, a multi-entry mechanism is proposed. Utilizing the pointer analysis algorithm, we implement a checker in TsmartGP to find uninitialized pointer errors in 13 real-world applications. Cppcheck and Clang Static Analyzer are chosen for comparison. The experimental results show that TsmartGP can find more errors while its accuracy rate is 100%, much higher than 3.1% for Cppcheck and 16.7% for Clang Static Analyzer. The demo video is available at https://youtu.be/IQlshemk6OA and TsmartGP can be downloaded from https://github.com/laoyaolandq/TsmartGP.

Yuexing Wang

Tsinghua University

Guang Chen

Tsinghua University

Min Zhou

Tsinghua University

Ming Gu

Tsinghua University

Jiaguang Sun

Tsinghua University

An enterprise system operates business by providing various services that are guided by set of certain business rules (BR) and constraints. These BR are usually written using plain Natural Language in operating procedures, terms and conditions, and other documents or in source code of legacy enterprise systems. For implementing the BR in a software system, expressing them as UML use-case specifications, or preparing for Merger & Acquisition (M&A) activity, analysts manually interpret the documents or try to identify constraints from the source code, leading to potential discrepancies and ambiguities. These issues in the software system can be resolved only after testing, which is a very tedious and expensive activity. To minimize such errors and efforts, we propose BuRRiTo framework consisting of automatic extraction of BR by mining documents and source code, ability to clean them of various anomalies like inconsistency, redundancies, conflicts, etc. and able to analyze the functional gaps present and performing semantic querying and searching.

Pavan Chittimalli

TCS Research

Kritika Anand

TCS Research

Shrishti Pradhan

TCS Research

Sayandeep Mitra

TCS Research

Chandan Prakash

TCS Research

India

Rohit Shere

TCS Research

Ravindra Naik

TCS Research, TRDDC, India

India

Programming is typically a difficult and repetitive task. Programmers encounter endless problems during programming, and they often need to write similar code over and over again. To prevent programmers from reinventing wheels thus increase their productivity, we propose a context-aware code-to-code recommendation tool named Lancer. With the support of a Library-Sensitive Language Model (LSLM) and the BERT model, Lancer is able to automatically analyze the intention of the incomplete code and recommend relevant and reusable code samples in real-time. code, and datasets can be found. A video demonstration of Lancer can be found at https://youtu.be/tO9nhqZY35g. Lancer is open source and the code is available at https://github.com/sfzhou5678/Lancer.

Shufan Zhou

School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University

Beijun Shen

School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University

Hao Zhong

Shanghai Jiao Tong University

China

We present TestCov, a tool for robust test-suite execution and test-coverage measurement on C programs. TestCov executes program tests in isolated containers to ensure system integrity and reliable resource control. The tool provides coverage statistics per test and for the whole test suite. TestCov uses the simple, XML-based exchange format for test-suite specifications that was established as standard by Test-Comp. TestCov has been successfully used in Test-Comp ’19 to execute almost 9 million tests on 1720 different programs. The source code of TestCov is released under the open-source license Apache 2.0 and available at https://gitlab.com/sosy-lab/software/test-suite-validator. A full artifact, including a demonstration video, is available at https://doi.org/10.5281/zenodo.3418726.

Dirk Beyer

LMU Munich

Germany

Thomas Lemberger

LMU Munich

Germany

We present Prema, a tool for Precise Requirement Editing, Modeling and Analysis. It can be used in various fields for describing precise requirements using formal notations and performing rigorous analysis. By parsing the requirements written in formal modeling language, Prema is able to get a model which aptly depicts the requirements. It also provides different rigorous verification and validation techniques to check whether the requirements meet users’ expectation and find potential errors. We show that our tool can provide a unified environment for writing and verifying requirements without using tools that are not well inter-related. For experimental demonstration, we use the requirements of the automatic train protection (ATP) system of CASCO signal co. LTD., the largest railway signal control system manufacturer of China. The code of the tool cannot be released here because the project is commercially confidential. However, a demonstration video of the tool is available at https://youtu.be/BX0yv8pRMWs.

Yihao Huang

East China Normal University

Jincao Feng

East China Normal University

Hanyue Zheng

East China Normal University

Jiayi Zhu

East China Normal University

Shang Wang

East China Normal University

Siyuan Jiang

Eastern Michigan University

Weikai Miao

Shanghai Key Lab for Trustworthy Computing, School of Computer Science and Software Engineering, East China Normal University

Geguang Pu

East China Normal University&Shanghai Trusted Industrial Control Platform Co., Ltd

Software engineering has seen much progress in recent past including introduction of new methodologies, new paradigms for software teams, and from smaller monolithic applications to complex, intricate, and distributed software applications. However, the way we represent, discuss, and collaborate on software applications throughout the software development life cycle is still primarily using the source code, textual representations, or charts on 2D computer screens - the confines of which have long limited how we visualize and comprehend software systems. In this paper, we present XRaSE, a novel prototype implementation that leverages augmented reality to visualize a software application as a virtually tangible entity. This immersive approach is aimed at making activities like application comprehension, architecture analysis, knowledge communication, and analysis of a software’s dynamic aspects, more intuitive, richer and collaborative. A video demonstration is available at https://youtu.be/_BYYnayA1FE.

Rohit Mehra

Accenture Labs, India

India

Vibhu Saujanya Sharma

Accenture Labs

Vikrant Kaulgud

Accenture Labs, India

India

Sanjay Podder

Accenture

India

The smart contract cannot be modified when it has been deployed on a blockchain. Therefore, it must be given thoroughly test before its being deployed. Mutation testing is considered as a practical test methodology to evaluate the adequacy of software testing. In this paper, we introduce MuSC, a mutation testing tool for Ethereum Smart Contract (ESC). It can generate numerous mutants at a fast speed and supports the automatic operations such as creating test nets, deploying and executing tests. Specially, MuSC implements a set of novel mutation operators w.r.t ESC programming language, Solidity. Therefore, it can expose the defects of smart contracts to a certain degree. The demonstration video of MuSC is available at https://youtu.be/3KBKXJPVjbQ, and the source code can be downloaded at https://github.com/belikout/MuSC-Tool-Demo-repo.

Zixin Li

Nanjing University

Haoran Wu

State Key Laboratory for Novel Software Technology, Nanjing University

Jiehui Xu

Nanjing University

Xingya Wang

State Key Laboratory for Novel Software Technology, Nanjing University

Lingming Zhang

The University of Texas at Dallas

United States

Zhenyu Chen

Nanjing University

China

Swarm-based verification methods split a verification problem into a large number of independent simpler tasks and so exploit the availability of large numbers of cores to speed up verification. Lazy-CSeq is a BMC-based bug-finding tool for C programs using POSIX threads that is based on sequentialization. Here we present the tool VeriSmart 2.0, which extends Lazy-CSeq with a swarm-based bug-finding method. The key idea of this approach is to constrain the interleavings such that context switches can only happen within selected tiles (more specifically, contiguous code segments within the individual threads). This under-approximates the program’s behaviors, with the number and size of tiles as additional parameters, which allows us to vary the complexity of the tasks. Overall, this significantly improves peak memory consumption and (wall-clock) analysis time.

Sources: http://www.cs.sun.ac.za/~bfischer/verismart.tgz

Bernd Fischer

Stellenbosch University

South Africa

Salvatore La Torre

Università degli Studi di Salerno

Italy

Gennaro Parlato

University of Molise

Deep neural networks~(DNNs) are increasingly expanding their real-world applications across domains, e.g., image processing, speech recognition and natural language processing. However, there is still limited tool support for DNN testing in terms of test data quality and model robustness. In this paper, we introduce a mutation testing-based tool for DNNs, DeepMutation++, which facilitates the DNN quality evaluation, supporting both feed-forward neural networks~(FNNs) and stateful recurrent neural networks~(RNNs). It not only enables to statically analyze the robustness of a DNN model against the input as a whole, but also allows to identify the vulnerable segments of a sequential input (e.g. audio input) by runtime analysis. It is worth noting that DeepMutation++ specially features the support of RNNs mutation testing. The tool demo video can be found on the project website https://sites.google.com/view/deepmutationpp.

Qiang Hu

Kyushu University, Japan

Lei Ma

Kyushu University

Japan

Xiaofei Xie

Nanyang Technological University

Bing Yu

Kyushu University, Japan

Yang Liu

Nanyang Technological University, Singapore

Singapore

Jianjun Zhao

Kyushu University

Japan

An effective way to maximize code coverage in software tests is through dynamic symbolic execution, a technique that uses constraint solving to systematically explore a program’s state space. We introduce an open-source dynamic symbolic execution framework called Manticore for analyzing binaries and Ethereum smart contracts. Manticore’s flexible architecture allows it to support both traditional and exotic execution environments, and its API allows users to customize their analysis. Here, we discuss Manticore’s architecture and demonstrate the capabilities we have used to find bugs and verify the correctness of code for our commercial clients.

Mark Mossberg

Trail of Bits

Felipe Manzano

Trail of Bits

Eric Hennenfent

Trail of Bits

Alex Groce

Trail of Bits

Gustavo Grieco

Trail of Bits

Josselin Feist

Trail of Bits

Trent Brunson

Trail of Bits

Artem Dinaburg

Trail of Bits

Concurrency vulnerabilities are extremely harmful and can be frequently exploited to launch severe attacks. Due to the non-determinism of multithreaded executions, it is very difficult to detect them. Recently, data race detectors and techniques based on maximal casual model have been applied to detect concurrency vulnerabilities. However, the former are ineffective and the latter report many false negatives. In this paper, we present CONVUL, an effective tool for concurrency vulnerability detection. CONVUL is based on exchangeable events, and adopts novel algorithms to detect three major kinds of concurrency vulnerabilities. To illustrate the competitiveness of CONVUL, we performed a comparison with three widely-used data race detectors and one recent tool based on maximal casual model. In our experiments, CONVUL detected 9 of 10 known vulnerabilities and found 6 zero-day vulnerabilities on MySQL, while other tools only detected at most 3 out of these 16 vulnerabilities. Our tool and data are available at CONVUL web page: https://sites.google.com/site/convultool. A demonstration video is available at https://youtu.be/-26C6ULxtbk

Ruijie Meng

University of Chinese Academy of Sciences

Biyun Zhu

University of Chinese Academy of Sciences

Hao Yun

University of Chinese Academy of Sciences

Haicheng Li

University of Chinese Academy of Sciences

Yan Cai

Institute of Software, Chinese Academy of Sciences

China

Zijiang Yang

Western Michigan University

Model Driven Engineering (MDE) techniques raise the level of abstraction at which developers construct software. However, modern cyber-physical systems are becoming more prevalent and complex and hence software models that represent the structure and behavior of such systems still tend to be large and complex. These models may have numerous if not infinite possible behaviors, with complex communications between their components. Appropriate software testing techniques to generate test cases with high coverage rate to put these systems to test at the model-level (without the need to understand the underlying code generator or refer to the generated code) are therefore important. Concolic testing, a hybrid testing technique that benefits from both concrete and symbolic execution, gains a high execution coverage and is used extensively in the industry for program testing but not for software models. In this paper, we present a novel technique and its tool mCUTE1 , an open source 2 model-level concolic testing engine. We describe the implementation of our tool in the context of Papyrus-RT, an open source Model Driven Engineering (MDE) tool based on UML-RT, and report the results of validating our tool using a set of benchmark models.

Reza Ahmadi

Queen's University

Karim Jahed

Queen's University

Juergen Dingel

Queen's University, Kingston, Ontario

ACM SIGSOFT Distinguished Paper Award

Game testing has been long recognized as a notoriously challenging task, which mainly relies on manual playing and scripting based testing in game industry. Even until recently, automated game testing still remains to be largely untouched niche. A key challenge is that game testing often requires to play the game as a sequential decision process. A bug may only be triggered until completing certain difficult intermediate tasks, which requires a certain level of intelligence. The recent success of deep reinforcement learning (DRL) sheds light on advancing automated game testing, without human competitive intelligent support. However, the existing DRLs mostly focus on winning the game rather than game testing. To bridge the gap, in this paper, we first perform an in-depth analysis of 1349 real bugs from four real-world commercial game products. Based on this, we propose four oracles to support automated game testing, and further propose Wuji, an on-the-fly game testing framework, which leverages evolutionary algorithm, DRL and multi-objective optimization to perform automatic game testing. Wuji balances between winning the game and exploring the space of the game. Winning the game allows the agent to make progress in the game, while space exploration increases the possibility of discovering bugs. We conduct a large-scale evaluation on a simple game and two popular commercial games. The results demonstrate the effectiveness of Wuji in exploring space and detecting bugs. Moreover, Wuji found 3 previously unknown bugs, which have been confirmed by the developers, in the commercial games.

Yan Zheng

Tianjin University

Singapore

Xiaofei Xie

Nanyang Technological University

Ting Su

ETH Zurich

Lei Ma

Kyushu University

Japan

Jianye Hao

Tianjin University

Zhaopeng Meng

Tianjin University

Yang Liu

Nanyang Technological University, Singapore

Singapore

Ruimin Shen

Fuxi AI Lab in Netease

Yinfeng Chen

Fuxi AI Lab in Netease

Changjie Fan

Fuxi AI Lab in Netease

Due to the popularity of deep learning (DL) applications, testing DL libraries are becoming more and more important. Different from traditional testing, for which output is asserted definitely (e.g., an output is compared with an oracle for equality), testing deep learning libraries often requires to perform oracle approximations, i.e., the output is allowed to be within a restricted range of the oracle. However, oracle approximations have not been studied in prior empirical work that focuses on traditional testing practices. The prevalence, common practices, evolution, and maintenance challenges of oracle approximations remain unknown. In this work, we studied oracle approximation assertions that are implemented in four popular deep learning libraries. Our study shows that oracle approximation assertions are a significant portion among all the assertions in the test suites of deep learning libraries. We identify the commonly-used oracle types when there are approximations being performed on oracles through a comprehensive manual study. In addition, we find that developers frequently modify code on oracle approximations, i.e., using a different approximation API, modifying the oracle or the output from the code under test, and using a different threshold value. Finally, we performed in-depth studies to understand the reasons behind the evolution of oracle approximation assertions and our findings reveal maintenance challenges.

Mahdi Nejadgholi

Concordia University

Jinqiu Yang

Concordia University, Montreal, Canada

We present techniques for automatically inferring formal properties of feed-forward neural networks. We observe that a significant part (if not all) of the logic of feed forward networks is captured in the activation status (on or off) of its neurons. We propose to extract patterns based on neuron decisions as preconditions that imply certain desirable output property e.g., the prediction being a certain class. Together, the inferred preconditions and the output property form a {\em contract} for the network. We present techniques to extract input properties} encoding convex predicates on the input space that imply given output properties and layer properties, representing network properties captured in the hidden layers that imply the desired output behavior. We apply our techniques on networks for the MNIST and ACASXU applications. Our experiments highlight the use of the inferred properties in a variety of tasks, such as explaining predictions, providing robustness guarantees, simplifying proofs, and network distillation.

Divya Gopinath

Carnegie Mellon University

Hayes Converse

The University of Texas at Austin

Corina S. Pasareanu

Carnegie Mellon University Silicon Valley, NASA Ames Research Center

Ankur Taly

Google

Deep Learning (DL) has recently achieved tremendous success in various application domains. A variety of DL frameworks and platforms play a key role to catalyze such progress. However, the differences in architecture designs and implementations of existing frameworks and platforms bring new challenges for DL software development and deployment. Till now, there is no study on how various mainstream frameworks and platforms influence both DL software development and deployment in practice.

To fill this gap, we take the first step towards understanding how the most widely-used DL frameworks and platforms support the DL software development and deployment. We conduct a systematic study on these frameworks and platforms by using two types of DNN architectures and three popular datasets. (1) For development process, we investigate the prediction accuracy under the same runtime training configuration or same model weights/biases. We also study the adversarial robustness of trained models by leveraging the existing adversarial attack techniques.The experimental results show that the {computing differences} across frameworks could result in an obvious prediction accuracy decline, which should draw the attention of DL developers. (2) For deployment process, we investigate the prediction accuracy and performance (refers to time cost and memory consumption) when the trained models are migrated/quantized from PC to real mobile devices and web browsers. The DL platform study unveils that the migration and quantization still suffer from compatibility and reliability issues. Meanwhile, we find several DL software bugs by using the results as a benchmark. We further validate the results through bug confirmation from stakeholders and industrial positive feedback to highlight the implications of our study. Through our study, we summarize practical guidelines, identify challenges and pinpoint new research directions, such as understanding the characteristics of DL frameworks and platforms, avoiding compatibility/reliability issues, detecting DL software bugs, and reducing time cost and memory consumption towards developing and deploying high quality DL systems effectively.

Qianyu Guo

Tianjin University

Sen Chen

Nanyang Technological University, Singapore

Singapore

Xiaofei Xie

Nanyang Technological University

Lei Ma

Kyushu University

Japan

Qiang Hu

Kyushu University, Japan

Hongtao Liu

Tianjin University

Yang Liu

Nanyang Technological University, Singapore

Singapore

Jianjun Zhao

Kyushu University

Japan

Li Xiaohong

TianJin University

China

Deep neural network (DNN) has been widely applied to safety-critical scenarios such as autonomous vehicle, security surveillance, and cyber-physical control systems. Yet, the incorrect behaviors of DNNs can lead to severe accidents and tremendous losses due to hidden defects. In this paper, we present DeepHunter, a general-purpose fuzzing framework for detecting defects of DNNs. DeepHunter is inspired by traditional grey-box fuzzing and aims to increase the overall test coverage by applying adaptive heuristics according to runtime feedback. Specifically, DeepHunter provides a series of seed selection strategies, metamorphic mutation strategies, and testing criteria customized to DNN testing; all these components support multiple built-in configurations which are easy to extend. We evaluated DeepHunter on two popular datasets and the results demonstrate the effectiveness of DeepHunter in achieving coverage increase and detecting real defects. A video demonstration which showcases the main features of DeepHunter can be found at https://youtu.be/s5DfLErcgrc.

Xiaofei Xie

Nanyang Technological University

Hongxu Chen

Nanyang Technological University

Yi Li

Nanyang Technological University

Singapore

Lei Ma

Kyushu University

Japan

Yang Liu

Nanyang Technological University, Singapore

Singapore

Jianjun Zhao

Kyushu University

Japan