CoVeriTeam Service: Verification as a Service Beyer, Dirk; Kanav, Sudeep; Wachowitz, Henrik
2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion),
05/2023
Conference Proceeding
Odprti dostop
The research community has developed numerous tools for solving verification problems, but we are missing a common web interface for executing them. This means, users have to commit to install and ...execute each new tool (version) on their local machine. We propose to use CoVeriTeam Service to make it easy for verification researchers to experiment with new verification tools. CoVeriTeam has already unified the command-line interface, and reduced the burden by taking care of tool installation and isolated execution. The new web service in addition enables tool developers to make their tools accessible on the web and users to include verification tools in their work flow. There are already further applications of our service: The 2023 competitions on software verification and testing used the service for their integration testing, and we propose to use CoVeriTeam Service for incremental verification as part of a continuous-integration process.
Demonstration video: https://youtu.be/0Ao0ZogSu1U
Demonstration service: https://coveriteam-service.sosy-lab.org
The SZZ algorithm for identifying bug-inducing changes has been widely used to evaluate defect prediction techniques and to empirically investigate when, how, and by whom bugs are introduced. Over ...the years, researchers have proposed several heuristics to improve the SZZ accuracy, providing various implementations of SZZ. However, fairly evaluating those implementations on a reliable oracle is an open problem: SZZ evaluations usually rely on (i) the manual analysis of the SZZ output to classify the identified bug-inducing commits as true or false positives; or (ii) a golden set linking bug-fixing and bug-inducing commits. In both cases, these manual evaluations are performed by researchers with limited knowledge of the studied subject systems. Ideally, there should be a golden set created by the original developers of the studied systems.
We propose a methodology to build a "developer-informed" oracle for the evaluation of SZZ variants. We use Natural Language Processing (NLP) to identify bug-fixing commits in which developers explicitly reference the commit(s) that introduced a fixed bug. This was followed by a manual filtering step aimed at ensuring the quality and accuracy of the oracle. Once built, we used the oracle to evaluate several variants of the SZZ algorithm in terms of their accuracy. Our evaluation helped us to distill a set of lessons learned to further improve the SZZ algorithm.
Test-based automatic program repair has attracted a lot of attention in recent years. However, the test suites in practice are often too weak to guarantee correctness and existing approaches often ...generate a large number of incorrect patches.
To reduce the number of incorrect patches generated, we propose a novel approach that heuristically determines the correctness of the generated patches. The core idea is to exploit the behavior similarity of test case executions. The passing tests on original and patched programs are likely to behave similarly while the failing tests on original and patched programs are likely to behave differently. Also, if two tests exhibit similar runtime behavior, the two tests are likely to have the same test results. Based on these observations, we generate new test inputs to enhance the test suites and use their behavior similarity to determine patch correctness.
Our approach is evaluated on a dataset consisting of 139 patches generated from existing program repair systems including jGen-Prog, Nopol, jKali, ACS and HDRepair. Our approach successfully prevented 56.3% of the incorrect patches to be generated, without blocking any correct patches.
This book discusses the historical networking environment that gave rise to SDN, as well as the latest advances in SDN technology. It provides state of the art knowledge needed for successful ...deployment of an SDN, including how to explain to the non-technical business decision makers in an organization the potential benefits and risks, in shifting parts of a network to the SDN model; how to make intelligent decisions about when to integrate SDN technologies in a network; how to decide if an organization should be developing its own SDN applications or looking to acquire them from an outside vendor; how to accelerate the ability to develop an SDN application; discusses the evolution of the switch platforms that enable SDN; addresses when to integrate SDN technologies in a network; provides an overview of sample SDN applications relevant to different industries; includes practical examples of how to write SDN applications. --
FaCoY Kim, Kisub; Kim, Dongsun; Bissyandé, Tegawendé F. ...
2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE),
05/2018
Conference Proceeding
Odprti dostop
Code search is an unavoidable activity in software development. Various approaches and techniques have been explored in the literature to support code search tasks. Most of these approaches focus on ...serving user queries provided as natural language free-form input. However, there exists a wide range of use-case scenarios where a code-to-code approach would be most beneficial. For example, research directions in code transplantation, code diversity, patch recommendation can leverage a code-to-code search engine to find essential ingredients for their techniques. In this paper, we propose FaCoY, a novel approach for statically finding code fragments which may be semantically similar to user input code. FaCoY implements a query alternation strategy: instead of directly matching code query tokens with code in the search space, FaCoY first attempts to identify other tokens which may also be relevant in implementing the functional behavior of the input code. With various experiments, we show that (1) FaCoY is more effective than online code-to-code search engines; (2) FaCoY can detect more semantic code clones (i.e., Type-4) in BigCloneBench than the state-of-the-art; (3) FaCoY, while static, can detect code fragments which are indeed similar with respect to runtime execution behavior; and (4) FaCoY can be useful in code/patch recommendation.
The data race problem is common in the interrupt-driven program, and it is difficult to find as a result of complicated interrupt interleaving. Static analysis is a mainstream technology to detect ...those problems, however, the synchronization mechanism of interrupt is hard to be processed by the existing method, which brings many false alarms. Eliminating false alarms in static analysis is the main challenge for precisely data race detection.
In this paper, we present a framework of static analysis combined with program verification, which performs static analysis to find all potential races, and then verifies every race to eliminate false alarms. The experiment results on related race benchmarks show that our implementation finds all race bugs in the phase of static analysis, and eliminates all false alarms through program verification.
DaMAT: A Data-Driven Mutation Analysis Tool Viganò, Enrico; Cornejo, Oscar; Pastore, Fabrizio ...
2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion),
05/2023
Conference Proceeding
Odprti dostop
We present DaMAT, a tool that implements data-driven mutation analysis. In contrast to traditional code-driven mutation analysis tools it mutates (i.e., modifies) the data exchanged by components ...instead of the source of the software under test. Such an approach helps ensure that test suites appropriately exercise components interoperability --- essential for safety-critical cyber-physical systems. A user-provided fault model drives the mutation process. We have successfully evaluated DaMAT on software controlling a microsatellite and a set of libraries used in deployed CubeSats. A demo video of DaMAT is available at https://youtu.be/s5M52xWCj84
Randomized Differential Testing of RDF Stores Yang, Rui; Zheng, Yingying; Tang, Lei ...
2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion),
05/2023
Conference Proceeding
As a special kind of graph database systems, RDF stores have been widely used in many applications, e.g., knowledge graphs and semantic web. RDF stores utilize SPARQL as their standardized query ...language to store and retrieve RDF graphs. Incorrect implementations of RDF stores can introduce logic bugs that cause RDF stores to return incorrect query results. These logic bugs can lead to severe consequences and are likely to go unnoticed by developers. However, no available tools can detect logic bugs in RDF stores.
In this paper, we propose RD2, a Randomized Differential testing approach of RDF stores, to reveal discrepancies among RDF stores, which indicate potential logic bugs in RDF stores. The core idea of RD2 is to build an equivalent RDF graph for multiple RDF stores, and verify whether they can return the same query result for a given SPARQL query. Guided by the SPARQL syntax and the generated RDF graph, we automatically generate syntactically valid SPARQL queries, which can return non-empty query results with high probability. We further unify the formats of SPARQL query results from different RDF stores and find discrepancies among them. We evaluate RD2 on three popular and widely-used RDF stores. In total, we have detected 5 logic bugs in them. A video demonstration of RD2 is available at https://youtu.be/da7XlsdbRR4.
ActionsRemaker: Reproducing GitHub Actions Zhu, Hao-Nan; Guan, Kevin Z.; Furth, Robert M. ...
2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion),
05/2023
Conference Proceeding
Mining Continuous Integration and Continuous Delivery (CI/CD) has enabled new research opportunities for the software engineering (SE) research community. However, it remains a challenge to reproduce ...CI/CD build processes, which is crucial for several areas of research within SE such as fault localization and repair. In this paper, we present ActionsRemaker, a reproducer for GitHub Actions builds. We describe the challenges on reproducing GitHub Actions builds and the design of ActionsRemaker. Evaluation of ActionsRemaker demonstrates its ability to reproduce fail-pass pairs: of 180 pairs from 67 repositories, 130 (72.2%) from 43 repositories are reproducible. We also discuss reasons for unreproducibility. ActionsRemaker is publicly available at https://github.com/bugswarm/actions-remaker, and a demo of the tool can be found at https://youtu.be/flblSqoxeAk.
AutoTrainer Zhang, Xiaoyu; Zhai, Juan; Ma, Shiqing ...
2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE),
05/2021
Conference Proceeding
With machine learning models especially Deep Neural Network (DNN) models becoming an integral part of the new intelligent software, new tools to support their engineering process are in high demand. ...Existing DNN debugging tools are either post-training which wastes a lot of time training a buggy model and requires expertises, or limited on collecting training logs without analyzing the problem not even fixing them. In this paper, we propose AutoTrainer, a DNN training monitoring and automatic repairing tool which supports detecting and auto-repairing five commonly seen training problems. During training, it periodically checks the training status and detects potential problems. Once a problem is found, AutoTrainer tries to fix it by using built-in state-of-the-art solutions. It supports various model structures and input data types, such as Convolutional Neural Networks (CNNs) for image and Recurrent Neural Networks (RNNs) for texts. Our evaluation on 6 datasets, 495 models show that AutoTrainer can effectively detect all potential problems with 100% detection rate and no false positives. Among all models with problems, it can fix 97.33% of them, increasing the accuracy by 47.08% on average.
PDF
