Pinpointing the location where a given unit of functionality—or feature—was implemented is a demanding and time-consuming task, yet prevalent in most software maintenance or evolution efforts. To that extent, we present PANGOLIN, an Eclipse plugin that helps developers identifying features among the source code. It borrows Spectrum-based Fault Localization techniques from the software diagnosis research field by framing feature localization as a diagnostic problem. PANGOLIN prompts users to label system executions based on feature involvement, and subsequently presents its spectrum-based feature localization analysis to users with the aid of a color-coded, hierarchic, and navigable visualization which was shown to be effective at conveying diagnostic information to users. Our evaluation shows that PANGOLIN accurately pinpoints feature implementations and is resilient to misclassifications by users.

Bruno Miguel Sotto-Mayor de Castro Machado

IST, University of Lisbon

Alexandre Perez

Palo Alto Research Center

Rui Abreu

Instituto Superior Técnico, U. Lisboa & INESC-ID

Portugal

Recurrent neural network (RNN) has achieved great success in processing sequential inputs for applications such as automatic speech recognition, natural language processing and machine translation. However, quality and reliability issues of RNNs make them vulnerable to adversarial attacks and hinder their deployment in real-world applications. In this paper, we propose a quantitative analysis framework — DeepStellar — to pave the way for effective security and quality analysis of software systems powered by RNNs. DeepStellar is generic to handle various RNN architectures, including LSTM and GRU, scalable to work on industrial-grade RNN models, and extensible to develop customized analyzers and tools. We demonstrated that, with DeepStellar, users are able to design efficient test generation tools, and develop effective adversarial sample detectors. We evaluated the developed applications on three real RNN models, including speech recognition and image classification.
DeepStellar outperforms existing approaches three hundred times in generating defect-triggering tests and achieves 97% accuracy in detecting adversarial attacks. A video demonstration which shows the main features of DeepStellar is available at https://sites.google.com/view/deepstellar/home/tool-demo.

Xiaoning Du

Nanyang Technological University

Xiaofei Xie

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

Misuse of APIs happens frequently due to misunderstanding of API semantics and lack of documentation. An important category of API-related defects is the error handling defects, which may result in security and reliability flaws. These defects can be detected with the help of static program analysis, provided that error specifications are known. The error specification of an API function indicates how the function can fail. Writing error specifications manually is time-consuming and tedious. Therefore, automatic inferring the error specification from API usage code is preferred. In this paper, we present Ares, a tool for automatically inferring error specifications for C code through static analysis. we employ multiple heuristics to identify error handling blocks and infer error specifications by analyzing the corresponding condition logic. Ares is evaluated on 19 real world projects, and the results reveal that Ares outperforms the state-of-the-art tool APEx by 37% in precision. Ares can also identify more error specifications than APEx. Moreover, the specifications inferred from Ares help find dozens of API-related bugs in well-known projects such as OpenSSL, among them 10 bugs are confirmed by developers. Video: https://youtu.be/nf1QnFAmu8Q. Repository: https://github.com/lc3412/Ares.

Li Chi

Tsinghua University

Zuxing Gu

School of Software, Tsinghua University

China

Min Zhou

Tsinghua University

Ming Gu

Tsinghua University

Hongyu Zhang

The University of Newcastle

Australia

Modern software often exists in many different, yet similar versions and/or variants, usually derived from a common code base (e.g., via clone-and-own). In the context of product- line engineering, family-based-analysis has shown very promising potential for improving efficiency in applying quality-assurance techniques to variant-rich software, as compared to a variant- by-variant approach. Unfortunately, these strategies rely on an product-line representation superimposing all program variants in a syntactically well-formed, semantically sound and variant- preserving manner, which is manually hard to obtain in practice. We demonstrate the SiMPOSE methodology for automatically generating superimpositions of N given program versions and/or variants facilitating family-based analysis of variant-rich soft- ware. SiMPOSE is based on a novel N-way model-merging tech- nique operating at the level of control-flow automata (CFA) rep- resentations of C programs, CFAs constitute a unified program abstraction utilized by many recent software-analysis tools. We illustrate different merging strategies supported by SiMPOSE, namely variant-by-variant, N-way merging, incremental 2-way merging, and partition-based N/2-way merging, and demonstrate how SiMPOSE can be used to systematically compare their impact on efficiency and effectiveness of family-based unit-test generation. The SiMPOSE tool, the demonstration of its usage as well as related artifacts and documentation can be found at http://pi.informatik.uni-siegen.de/projects/variance/simpose.

Dennis Reuling

Software Engineering Group, University of Siegen

Germany

Udo Kelter

Software Engineering Group, University of Siegen

Sebastian Ruland

TU Darmstadt, Real-time Systems Lab

Malte Lochau

TU Darmstadt

Verification of programs continues to be a challenge and no single technique succeeds on all programs. In this paper we present VeriAbs, a reachability C program verifier that incorporates a portfolio of techniques implemented as four strategies, where a strategy is a set of techniques applied in a specific sequence. It selects a strategy based on the kind of loops in the program. We analysed the effectiveness of implemented strategies on the 3831 verification tasks from the ReachSafety category of the 8th International Competition on Software Verification (SV-COMP) 2019 and found that although simple classic techniques - explicit state model checking and bounded model checking, succeed on a majority of the programs, a wide range of further techniques are required to analyse the rest. A screencast of the tool is available at https://youtu.be/YHxB2V4U0gQ.

Mohammad Afzal

Tata Cosultancy Services

A Asia

Tata Cosultancy Services

Avriti Chauhan

Tata Cosultancy Services

Bharti Chimdyalwar

Tata Consultancy Services

Priyanka Darke

Tata Consultancy Services

Advaita Datar

Tata Consultancy Services Ltd

Shrawan Kumar

Tata Cosultancy Services

R Venkatesh

Tata Research Development and Design Centre

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

Smart pointers are widely used to prevent memory errors in modern C++ code. However, improper usage of smart pointers may also lead to common memory errors, which makes the code not as safe as expected. To avoid smart pointer errors as early as possible, we present a coding style checker to detect possible bad smart pointer usages during compile time, and notify programmers about bug-prone behaviors. The evaluation indicates that the currently available state-of-the-art static code checkers can only detect 25 out of 116 manually inserted errors, while our tool can detect all these errors. And we also found 521 bugs among 8 open source projects with only 4 false positives.

Xutong Ma

Institute of Software, Chinese Academy of Sciences

Jiwei Yan

Institute of Software, Chinese Academy of Sciences

Yaqi Li

Institute of Software, Chinese Academy of Sciences

Jun Yan

Institute of Software, Chinese Academy of Sciences

Jian Zhang

Institute of Software, Chinese Academy of Sciences

The fragmentation issue spreads over multiple mobile platforms such as Android, iOS, mobile web and even WeChat, which hinders test scripts from running across platforms. To reduce the cost of adapting scripts for various platforms, some existing tools apply conventional computer vision techniques to replay the same script on multiple platforms automatically. However, because these solutions can hardly identify dynamic or similar widgets, it becomes difficult for engineers to apply them in practice. In this paper, we present an image-driven tool, namely LIRAT, to record and replay test scripts cross platforms, solving the problem of test script cross-platform replay for the first time. LIRAT records screenshots and layouts of the widgets, and leverages image understanding techniques to locate them in the replay process. Based on accurate widget localization, LIRAT supports replaying test scripts across devices and platforms. We employed LIRAT to replay 25 scripts from 5 application across 8 Android devices and 2 iOS devices. The results show that LIRAT can replay 88% scripts on Android platforms and 60% on iOS platforms.

Shengcheng Yu

Nanjing University, China

China

Chunrong Fang

Nanjing University

Yang Feng

University of California, Irvine

United States

Wenyuan Zhao

Nanjing University

Zhenyu Chen

Nanjing University

China

Workflow underlies most process automation software, such as those for product lines, business processes, and scientific computing. However, current Cloud Computing based workflow systems cannot support real-time applications due to network latency, which limits their application in many IoT systems such as smart healthcare and smart traffic. Fog Computing extends the Cloud by providing virtualized computing resources close to the End Devices so that the response time of accessing computing resources can be reduced significantly. However, how to most effectively manage heterogeneous resources and different computing tasks in the Fog is a big challenge. In this paper, we introduce “FogWorkflowSim” an efficient and extensible toolkit for automatically evaluating resource and task management strategies in Fog Computing with simulated user-defined workflow applications. Specifically, FogWorkflowSim is able to: 1) automatically set up a simulated Fog Computing environment for workflow applications; 2) automatically execute user submitted workflow applications; 3) automatically evaluate and compare the performance of different computation offloading and task scheduling strategies with three basic performance metrics, including time, energy and cost. FogWorkflowSim can serve as an effective experimental platform for researchers in Fog based workflow systems as well as practitioners interested in adopting Fog Computing and workflow systems for their new software projects.

Xiao Liu

School of Information Technology, Deakin University

Australia

Lingmin Fan

School of Computer Science and Technology, Anhui University

Jia Xu

School of Computer Science and Technology, Anhui University

Xuejun Li

School of Computer Science and Technology, Anhui University

Lina Gong

School of Computer Science and Technology, Anhui University

John Grundy

Monash University

Australia

Yun Yang

Swinburne University of Technology

Spreadsheets are widely used but subject to various defects. In this paper, we present SGUARD to effectively detect spreadsheet defects. SGUARD learns spreadsheet features to cluster cells with similar computational semantics, and then refine these clusters to recognize anomalous cells as defects. SGUARD well balances the trade-off between the precision (87.8%) and recall rate (71.9%) in the defect detection, and achieves an F-measure of 0.79, exceeding existing spreadsheet defect detection techniques. We introduce the SGUARD implementation and its usage by a video presentation (https://youtu.be/gNPmMvQVf5Q), and provide its download repository for public access (https://github.com/sheetguard/sguard).

Da Li

State Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China

Huiyan Wang

State Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China

Chang Xu

Nanjing University

China

Ruiqing Zhang

Search Tech. Center Asia, Microsoft, Suzhou, China

Shing-Chi Cheung

Department of Computer Science and Engineering, The Hong Kong University of Science and Technology

China

Xiaoxing Ma

State Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University

Floating-point arithmetic is widely used in applications from several fields including scientific computing, machine learning, graphics, and finance. Many of these applications are rapidly adopting the use of GPUs to speedup computations. GPUs, however, have limited support to detect floating-point exceptions, making it difficult to software developers to detect unexpected exceptional cases in such applications. We present FPChecker, the first tool to automatically detect floating-point exceptions in GPU applications. FPChecker uses the clang/LLVM compiler to instrument GPU kernels and to detect floating-point exceptions in GPUs at runtime. Once an exception is detected, it reports to the programmer the code location of the exception as well as other useful information. The programmer can then use this information to avoid the exception, e.g., by modifying the application algorithm or changing its input. We present the design of FPChecker, an evaluation of the overhead of the tool, and a real-world case scenario on which the tool is used to identify a hidden exception. The slowdown of FPChecker is moderate ($1.5\times$ on average) and the code is publicly available as open source.

Ignacio Laguna

Lawrence Livermore National Laboratory

This paper presents PMExec, a tool that supports the execution of partial UML-RT models. To this end, the tool implements the following steps: static analysis, automatic refinement, and input-driven execution. The static analysis respects the execution semantics of UML-RT models is used to detect problematic model elements, i.e., elements that cause problems during execution due to the partiality. Then, the models are refined automatically using model transformation techniques, which mostly add decision points where missing information can be supplied. Third, the refined models are executed, and when the execution reaches the decision points, input required to continue the execution is obtained either interactively or from a script that captures how to deal with partial elements. We have evaluated PMExec using several use-cases that show that the static analysis, refinement, and application of user input can be carried out with reasonable performance, and that the overhead of approach, due to the refinement step, is manageable. (https://youtu.be/BRKsselcMnc)

Mojtaba Bagherzadeh

Queen's University

Canada

Karim Jahed

Queen's University

Nafiseh Kahani

Queen's University

Juergen Dingel

Queen's University, Kingston, Ontario

Mutation analysis, which introduces artificial defects into software systems, is the basis of mutation testing, a technique widely applied to evaluate and enhance the quality of test suites. However, despite the deep analogy between tests and formal proofs, mutation analysis has seldom been considered in the context of deductive verification. We propose mutation proving, a technique for analyzing verification projects that use proof assistants. We implemented our technique for the Coq proof assistant in a tool dubbed mCoq. mCoq applies a set of mutation operators to Coq definitions of functions and datatypes, inspired by operators previously proposed for functional programming languages. mCoq then checks proofs of lemmas affected by operator application. To make our technique feasible in practice, we implemented several optimizations in mCoq such as parallel proof checking. We applied mCoq to several medium and large scale Coq projects, and recorded whether proofs passed or failed when applying different mutation operators. We then qualitatively analyzed the mutants, and found several examples of weak and incomplete specifications. For our evaluation, we made many improvements to serialization of Coq code and even discovered a notable bug in Coq itself, all acknowledged by developers. We believe mCoq can be useful both to proof engineers for improving the quality of their verification projects and to researchers for evaluating proof engineering techniques.

Ahmet Celik

The University of Texas at Austin

Karl Palmskog

University of Texas at Austin

United States

Marinela Parovic

The University of Texas at Austin

Emilio Jesús Gallego Arias

MINES ParisTech

France

Milos Gligoric

The University of Texas at Austin

United States

Cryptographic primitives are ubiquitous for modern security. The correctness of their implementations is crucial to resist malicious attacks. Typical arithmetic computation of these C programs contains large numbers of non-linear operations, hence is challenging existing automatic C verification tools. We present an automated approach to verify cryptographic C programs. Our approach successfully verifies C implementations of various arithmetic operations used in NIST P-224, P-256, P-521 and Curve25519 in OpenSSL. During verification, we expose a bug and a few anomalies that have been existing for a long time. They have been reported to and confirmed by the OpenSSL community. Our results establish the functional correctness of these C implementations for the first time.

Jiaxiang Liu

Shenzhen University

China

Xiaomu Shi

Shenzhen University

Ming-Hsien Tsai

Academia Sinica, Taiwan

Bow-Yaw Wang

Academia Sinica

Bo-Yin Yang

Academia Sinica

Verification of multitasking embedded software requires taking into account its underlying operating system w.r.t. its scheduling policy and handling of task priorities in order to achieve a higher degree of accuracy. However, such comprehensive verification of multitasking embedded software together with its underlying operating system is very costly and impractical. To reduce the verification cost while achieving the desired accuracy, we propose a variant of CEGAR, named OiL-CEGAR (OS-in-the-Loop Counterexample-Guided Abstraction Refinement), where a composition of a formal OS model and an abstracted application program is used for comprehensive verification and is successively refined using the counterexamples generated from the composition model. The refinement process utilizes the scheduling information in the counterexample, which acts as a mini-OS to check the executability of the counterexample trace on the concrete program. Our experiments using a prototype implementation of OiL-CEGAR show that OiL-CEGAR greatly improves the accuracy and efficiency of property checking in this domain. It automatically removed all false alarms and accomplished property checking within an average of 476 seconds over a set of multitasking programs, whereas model checking using existing approaches over the same set of programs either showed an accuracy of under 11.1% or was unable to finish the verification due to timeout.

Dongwoo Kim

Kyungpook National University

South Korea

Yunja Choi

Kyungpook National University

South Korea

Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable forthcoming challenges. For example, C programmers regularly use inline assembly for low-level optimizations and system primitives. This usually results in rendering state-of-the-art formal analyzers developed for C ineffective. We thus propose TInA, the first automated, generic, verification-friendly and trustworthy lifting technique turning inline assembly into semantically equivalent C code, in order to take advantage of existing C analyzers. Extensive experiments on real-world C code with inline assembly (including GMP and ffmpeg) show the feasibility and benefits of TInA.

Frédéric Recoules

CEA LIST

Sebastien Bardin

CEA LIST

France

Richard Bonichon

CEA LIST

Laurent Mounier

Université Grenoble Alpes

Marie-Laure Potet

Université Grenoble Alpes