With the application of deep learning (DL) in signal detection, improving the robustness of classification models has received much attention, especially in automatic modulation classification (AMC) of electromagnetic signals. To obtain robust models, a large amount of electromagnetic signal data is required in the training and testing process. However, both the high cost of manual collection and the low quality of data samples from automatically generated data result in the defects of the AMC models. Therefore, it is important to generate electromagnetic data by data augmentation. In this paper, we propose a novel electromagnetic data augmentation tool, namely ElecDaug, which directs the metamorphic process by electromagnetic signal characteristics to achieve automatic data augmentation. Based on electromagnetic data pre-processing, transmission or time-frequency domains characteristic metamorphic, ElecDaug can augment the data samples to build robust AMC models. Preliminary experiments show that ElecDaugcan effectively augment available data samples for model repair. The video is at https://youtu.be/tqC0z5Sg1_k. Documentation and source code can be found here: https://github.com/ehhhhjw/tool_ElecDaug.git.

Jiawei He

Zhida Bao

Harbin Engineering University

Quanjun Zhang

Nanjing University

Weisong Sun

State Key Laboratory for Novel Software Technology, Nanjing University

China

Jiawei Liu

Nanjing University

China

Chunrong Fang

Nanjing University

China

Yun Lin

National University of Singapore

Singapore

Dynamic program analysis tools such as Eraser, Memcheck, or ThreadSanitizer abstract the contents of individual memory locations and store the abstraction results in a separate data structure called shadow memory. They then use this meta-information to efficiently implement the actual analyses. In this paper, we describe the implementation of an efficient symbolic shadow memory extension for the CBMC bounded model checker that can be accessed through an API, and sketch its use in the design of a new data race analyzer that is implemented by a code-to-code translation. Artifact/tool URL: shorturl.at/jzVZ0 Video URL: youtu.be/pqlbyiY5BLU

Bernd Fischer

Stellenbosch University, South Africa

South Africa

Salvatore La Torre

Università degli Studi di Salerno

Italy

Gennaro Parlato

University of Molise

Peter Schrammel

University of Sussex and Diffblue Ltd

United Kingdom

With the rapid development of autonomous driving systems (ADS), especially the increasing adoption of deep neural networks (DNNs) as their core components, effective quality assurance methods for ADS have attracted growing interests in both academia and industry. In this paper, we report a new testing platform ADEPT we have developed, aiming to provide practically realistic and comprehensive testing facilities for DNN-based ADS. ADEPT is based on the virtual simulator CARLA and provides numerous testing facilities such as scene construction, ADS importation, test execution and recording, etc. In particular, ADEPT features two distinguished test scenario generation strategies designed for autonomous driving. First, we make use of real-life accident reports from which we leverage natural language processing to fabricate abundant driving scenarios. Second, we synthesize physically-robust adversarial attacks by taking the feedback of ADS into consideration and thus are able to generate closed-loop test scenarios. The experiments confirm the efficacy of the platform. A video demonstrating the usage of ADEPT can be found at https://youtu.be/evMorf0uR_s.

Sen Wang

Nanjing University

Zhuheng Sheng

Nanjing University

Jingwei Xu

Taolue Chen

University of Surrey, UK

Junjun Zhu

Nanjing University

Shuhui Zhang

Nanjing University

Yuan Yao

Nanjing University

Xiaoxing Ma

Nanjing University

China

Dynamic taint analysis (DTA) is a popular approach to help protect JavaScript applications against injection vulnerabilities. In 2016, the ECMAScript 7 JavaScript language standard introduced many language features that most existing DTA tools for JavaScript do not support, e.g., the async/await keywords for asynchronous programming. We present Augur, a high-performance dynamic taint analysis for ES7 JavaScript that leverages VM-\textit{supported} instrumentation. Integrating directly with a public, stable instrumentation API gives Augur the ability to run with high performance inside the VM and remain resilient to language revisions. We extend the abstract-machine approach to DTA with semantics to handle asynchronous function calls. In addition to providing the classic DTA use case of injection vulnerability detection, Augur is highly configurable to support any type of taint analysis, making it useful outside of the security domain. We evaluated Augur on a set of 20 benchmarks, and observed a median runtime overhead of only 1.77×. We note a median performance improvement of 298% compared to the previous state-of-the-art Ichnaea.

Tool demo: https://www.youtube.com/watch?v=GczQ-2A58LE

Link to open source code repository: https://github.com/nuprl/augur

Mark W. Aldrich

Tufts University

United States

Alexi Turcotte

Northeastern University

United States

Matthew Blanco

Northeastern University

Frank Tip

Northeastern University

United States

Types in TypeScript play an important role in the correct usage of variables and APIs. Type errors such as variable or function misuse can be avoided with explicit type annotations. In this work, we introduce FlexType, an IDE extension that can be used on both JavaScript and TypeScript to infer types in an interactive or automatic fashion. We perform experiments with FlexType in JavaScript to determine how many types FlexType could resolve if it were to be used to migrate top JavaScript projects to TypeScript. FlexType is able to annotate 56.69% of all types with high precision and confidence including native and imported types from modules. In addition to the automatic inference, we believe the interactive Visual Studio Code extension is inherently useful in both TypeScript and JavaScript especially when resolving types is taxing for the developer.

The source code is available at GitHub and a video demonstration at https://youtu.be/4dPV05BWA8A.

Sivani Voruganti

UC Davis

Kevin Jesse

University of California at Davis, USA

United States

Prem Devanbu

Department of Computer Science, University of California, Davis

United States

Smart contracts are self-executing computer programs deployed on blockchain to enable trustworthy exchange of value without the need of a central authority. With the absence of documentation and specifications, routine tasks such as program understanding, maintenance, verification, and validation, remain challenging for smart contracts. In this paper, we propose a dynamic invariant detection tool, InvCon, for Ethereum smart contracts to mitigate this issue. The detected invariants can be used to not only support the reverse engineering of contract specifications, but also enable standard-compliance checking for contract implementations. InvCon provides a Web-based interface and a demonstration video of it is available at: https://youtu.be/Y1QBHjDSMYk.

Ye Liu

Nanyang Technological University

Yi Li

Nanyang Technological University, Singapore

Singapore

We developed a plugin for IntelliJ IDEA called AntiCopyPaster, which tracks the pasting of code fragments inside the IDE and suggests the appropriate Extract Method refactoring to combat the propagation of duplicates. Unlike the existing approaches, our tool is integrated with the developer’s workflow, and pro-actively recommends refactorings. Since not all code fragments need to be extracted, we develop a classification model to make this decision. When a developer copies and pastes a code fragment, the plugin searches for duplicates in the currently opened file, waits for a short period of time to allow the developer to edit the code, and finally inferences the refactoring decision based on a number of features.

Our experimental study on a large dataset of 18,942 code fragments mined from 13 Apache projects shows that AntiCopyPaster correctly recommends Extract Method refactorings with an F-score of 0.82. Furthermore, our survey of 59 developers reflects their satisfaction with the developed plugin’s operation. The plugin and its source code are publicly available on GitHub at https://github.com/JetBrains-Research/anti-copy-paster. The demonstration video can be found on YouTube: https://www.youtube.com/watch?v=_wwHg-qFjJY.

Eman Abdullah AlOmar

Stevens Institute of Technology

United States

Anton Ivanov

HSE University

Zarina Kurbatova

JetBrains Research

Russia

Yaroslav Golubev

JetBrains Research

Serbia

Mohamed Wiem Mkaouer

Rochester Institute of Technology

United States

Ali Ouni

ETS Montreal, University of Quebec

Canada

Timofey Bryksin

JetBrains Research

Cyprus

Le Nguyen

Rochester Institute of Technology

Amit Kini

Rochester Institute of Technology

Aditya Thakur

Rochester Institute of Technology

To face the climate change, Android developers urge to become green software developers. But how to ensure carbon-efficient mobile apps at large? In this paper, we introduce $ecoCode$, a SonarQube plugin able to highlight code structures that are smelly from an energy perspective. It is based on a curated list of energy code smells likely to impact negatively the battery lifespan of Android-powered devices. The $ecoCode$ plugin enables analysis of any native Android project written in Java in order to enforce green code.

Olivier Le Goaër

LIUPPA, Université de Pau et des Pays de l'Adour

France

Julien Hertout

Snapp'

As software systems continue to grow in complexity and scale, deploying and delivering them becomes increasingly difficult. In this work, we develop DeployQA, a novel QA bot that automatically answers software deployment questions over user manuals and Stack Overflow posts. DeployQA is built upon RoBERTa. To bridge the gap between natural language and the domain of software deployment, we propose three adaptations in terms of vocabulary, pre-training, and fine-tuning, respectively. We evaluate our approach on our constructed DeQuAD dataset. The results show that DeployQA remarkably outperforms baseline methods by leveraging the three domain adaptation strategies.

Guan Jie Qiu

School of Software, Shanghai Jiao Tong University

Diwei Chen

School of Software, Shanghai Jiao Tong University

Shuai Zhang

School of Software, Shanghai Jiao Tong University

Yitian Chai

School of Software, Shanghai Jiao Tong University

Xiaodong Gu

Shanghai Jiao Tong University, China

China

Beijun Shen

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

Refactoring software can be hard and time-consuming. Several refactoring tools assist developers in reaching more readable and maintainable code. However, most of them are characterized by long feedback loops that impoverish their refactoring experience. We believe that we can reduce this problem by focusing on the concept of Live Refactoring and its main principles: the live recommendation and continuous visualization of refactoring candidates, and the immediate visualization of results from applying a refactoring to the code. Therefore, we implemented a Live Refactoring Environment that identifies, suggests, and applies Extract Method refactorings. To evaluate our approach, we carried out an empirical experiment. Early results showed us that our refactoring environment improves several code quality aspects, being well received, understood, and used by the experiment participants. The source code of our tool is available on: https://github.com/saracouto1318/LiveRef. Its demonstration video can be found at: https://youtu.be/_jxx21ZiQ0o.

Sara Fernandes

FEUP, Universidade do Porto

Portugal

Ademar Aguiar

FEUP, Universidade do Porto

Portugal

André Restivo

LIACC, Universidade do Porto, Porto, Portugal

Portugal

Automatic vulnerability detection is of paramount importance to promote the security of an application and should be exercised at the earliest stages within the software development life cycle (SDLC) to reduce the risk of exposure. Despite the advancements with state-of-the-art deep learning techniques in software vulnerability detection, the development environments are not yet leveraging their performance. In this work, we integrate the Transformers architecture, one of the main highlights of advances in deep learning for Natural Language Processing, within a developer-friendly tool for code security. We introduce VDet for Java, a transformer-based VS Code extension that enables one to discover vulnerabilities in Java files. Our preliminary model evaluation presents an accuracy of 85.8% for multi-label classification and can detect up to 21 vulnerability types. The demonstration of our tool can be found at https://youtu.be/OjiUBQ6TdqE.

Cláudia Mamede

FEUP, U.Porto

Eduard Pinconschi

FEUP, U.Porto

Rui Abreu

Faculty of Engineering, University of Porto, Portugal

Portugal

Feature modeling is widely used to systematically model features of variant-rich software systems and their dependencies. By translating feature models into propositional formulas and analyzing them with solvers, a wide range of automated analyses across all phases of the software development process become possible. Most solvers only accept formulas in conjunctive normal form (CNF), so an additional transformation of feature models is often necessary. However, it is unclear whether this transformation has a noticeable impact on analyses. In this paper, we compare three transformations (i.e., distributive, Tseitin, and Plaisted-Greenbaum) for bringing feature-model formulas into CNF. We analyze which transformation can be used to correctly perform feature-model analyses and evaluate three CNF transformation tools (i.e., FeatureIDE, KConfigReader, and KClause) on a corpus of 22 real-world feature models. Our empirical evaluation illustrates that some CNF transformations do not scale to complex feature models or even lead to wrong results for certain analyses. Further, the choice of the CNF transformation can substantially influence the performance of subsequent analyses.

Elias Kuiter

Otto-von-Guericke-University Magdeburg

Sebastian Krieter

University of Ulm

Chico Sundermann

University of Ulm

Germany

Thomas Thüm

University of Ulm

Germany

Gunter Saake

University of Magdeburg, Germany

Stochastic model checking can automatically verify and analyse the software-driven autonomous systems with stochastic behaviors, which is a formal verification technique based on system models. When coping with large-scale systems, it suffers from state space explosion problem very seriously. Model abstraction is a potential technique for mitigating this problem. At present, only a few properties specified by PCTL (Probabilistic Computation Tree Logic), such as probabilistic safety and probabilistic reachability, can be preserved in the practical model abstraction of stochastic model checking, which are the proper subset of PCTL* properties. For dealing with this, an effective and efficient three-valued model abstraction framework for full PCTL* stochastic model checking is proposed in this paper. We propose a new abstract model to preserve full PCTL* properties for nondeterministic and probabilistic system, which orthogonally integrates interval probability of transition and game for nondeterminism. A game-based three-valued PCTL* stochastic model checking algorithm is developed to verify abstract model, and a BPSO (binary particle swarm optimization) algorithm integrated with sample learning is designed to refine the indefinite result of three-valued PCTL* stochastic model checking abstract model. It is proved that full PCTL* properties are preserved when the result of three-valued stochastic model checking is definite, and the efficiency of this framework is demonstrated by some large cases.

Yang Liu

Shanghai Maritime University/National University of Singapore

Yan Ma

Nanjing University of Finance and Economics / National University of Singapore

Yongsheng Yang

Shanghai Maritime University

We propose Janus, an approach for finding incompleteness bugs in SMT solvers. The key insight is to mutate SMT formulas with local weakening and strengthening rules that preserve the satisfiability of the seed formula. The generated mutants are used to test SMT solvers for incompleteness bugs, i.e., inputs on which the SMT solver unexpectedly returns unknown. We realized Janus on top of the SMT solver fuzzing framework YinYang. From June to August 2021, we stress-tested the two state-of-the-art SMT solvers Z3 and CVC5 with Janus and totally reported 32 incompleteness bugs. Out of these, 24 have been confirmed as unique bugs and 8 are already fixed by the developers. Our diverse bug findings uncovered functional, regression, and performance bugs—several surprising enough to trigger discussions among the developers sharing their in-depth analysis.

Mauro Bringolf

ETH Zurich

Dominik Winterer

ETH Zurich

Switzerland

Zhendong Su

ETH Zurich

Switzerland

Linear temporal logic (LTL) satisfiability checking is a fundamental and hard problem (PSPACE-complete). In this paper, we explore checking LTL satisfiability via end-to-end learning, so that we can take only polynomial time to check LTL satisfiability. Existing approaches have shown that it is possible to leverage end-to-end neural networks to predict the Boolean satisfiability problem with performance considerably higher than random guessing. Inspirited by their work, we study two interesting questions: can end-to-end neural networks check LTL satisfiability, and can neural networks learn the semantics of LTL. To this end, we train some neural networks with different architectures to explore the potential of neural networks on LTL satisfiability checking. We demonstrate that neural networks can indeed capture some effective biases for LTL satisfiability checking by training. Besides, designing a special architecture matching some logical properties of LTL, e.g., recursive property, permutation invariance, and sequentiality, can provide a better inductive bias. We also show the competitive results of neural networks compared with the state-of-the-art approaches, i.e., nuXmv and Aalta, on large scale datasets.

Weilin Luo

School of Computer Science and Engineering, Sun Yat-sen University

Hai Wan

School of Data and Computer Science, Sun Yat-sen University

China

Delong Zhang

SUN YAT-SEN UNIVERSITY

Jianfeng Du

Guangdong University of Foreign Studies

Hengdi Su

SUN YAT-SEN UNIVERSITY

Deep learning has become a promising programming paradigm in software development, owing to its surprising performance in solving many challenging tasks. Deep neural networks (DNNs) are increasingly being deployed in practice, but are limited on resource-constrained devices owing to their demand for computational power. Quantization has emerged as a promising technique to reduce the size of DNNs with comparable accuracy as their floating-point numbered counterparts. The resulting quantized neural networks (QNNs) can be implemented energy-efficiently. Similar to their floating-point numbered counterparts, quality assurance techniques for QNNs, such as testing and formal verification, are essential but are currently less explored. In this work, we propose a novel and efficient formal verification approach for QNNs. In particular, we are the first to propose an encoding that reduces the verification problem of QNNs into the solving of integer linear constraints, which can be solved using off-of-the-shelf solvers. Our encoding is both sound and complete. We demonstrate the application of our approach on local robustness verification and maximum robustness radius computation. We implement our approach in a prototype tool QVIP and conduct a thorough evaluation. Experimental results on QNNs with different quantization bits confirm the effectiveness and efficiency of our approach, e.g., our approach is two orders of magnitude faster and able to solve more verification tasks in the same time limit than the state-of-the-art methods.

Yedi Zhang

ShanghaiTech University

Zhe Zhao

ShanghaiTech University

China

Guangke Chen

ShanghaiTech University

China

Fu Song

ShanghaiTech University

China

Min Zhang

East China Normal University

China

Taolue Chen

Birkbeck University of London

United Kingdom

Jun Sun

Singapore Management University

Singapore