KLEEF is a complete overhaul of the KLEE symbolic execution engine for LLVM , fine-tuned for a robust analysis of industrial C/C++ code. KLEEF natively handles complex data structures, such as trees, linked lists, and dynamically allocated arrays, via lazy initialization and symcrete values. KLEEF has fine-tuned modes for both maximal test coverage generation and reproducing error traces, in particular reaching a specific point in the program. In the paper, we describe the above features and a competition configuration of KLEEF .

One common way to speed up the find operation within a set of text files involves a trigram index. This structure is merely a map from a trigram (sequence consisting of three characters) to a set of files which contain it. When searching for a pattern, potential file locations are identified by intersecting the sets related to the trigrams in the pattern. Then, the search proceeds only in these files. However, in a code repository, the trigram index evolves across different versions. Upon checking out a new version, this index is typically built from scratch, which is a time-consuming task, while we want our index to have almost zero-time startup. Thus, we explore the persistent version of a trigram index for full-text and key word patterns search. Our approach just uses the current version of the trigram index and applies only the changes between versions during checkout, significantly enhancing performance. Furthermore, we extend our data structure to accommodate CamelHump search for class and function names.

UTBot is a tool for automated unit test generation, that generates ready-to-use Python test cases. It uses two approaches for finding input values: fuzzing and dynamic symbolic execution, which run in parallel. In this paper, we report the UTBot results at the SBFT 2024 Python tool competition.

In recent times, program analysis methods are increasingly being used to improve the quality of software projects. One of the easiest ways to apply such methods is to use an automatic test generator. There are many automatic test generation tools exist for popular programming languages, each employing diverse methods of program analysis. UTBot, a JUnit test generator, is one such tool that leverages symbolic execution for test suite generation. However, symbolic execution has limitations that restrict its practicality usage for real-world programs. In this work, we addressed this limitation by implementing fuzzing as part of the tool. Fuzzing is a widely adopted and effective dynamic program analysis method involving the injection of invalid, unexpected, or random data to discover vulnerabilities and bugs in a program. The implemented fuzzing module, integrated into the UTBot tool, took part in the SBFT-2023 test generator competition. During competition the developed module was applied to realworld programs. The results demonstrated that fuzzing is wellsuited for addressing test generation challenges and can be used to overcome the limitations of symbolic execution.

Symbolic execution (SE) is one of the most promising techniques for automated unit test generation, which is claimed to streamline the testing process and reduce developers' effort. There are symbolic execution engines working for Java, C, C#, C++, Python,. NET. The KLEE dynamic symbolic execution engine is one of the most elaborated ones - it is built on top of the LLVM compiler infrastructure and can automatically generate inputs for C code unit testing. There are numerous attempts to apply KLEE to real-life software projects, while the industry experience still shows little transfer from research to practice. The extensions to popular integrated development environments (IDEs) are supposed to be breaking down this barrier. As far as there are not so many working tools like this, we share our experience of implementing the KLEE-based Visual Studio Code and CLion extensions for generating ready-to-use test cases - UnitTestBot for C code- and describe the challenges we had to rise to. We also share the solutions we came up with: without introducing “new” techniques, we made automated unit test generation really automated and supplemented it with the simple wizard interface. That was enough for turning an effective but demanding technology into a user-friendly tool, which is easy to adopt. Finally, we provide examples of running UnitTestBot on the open-source projects as well as Huawei nonpublic code.

UTBot is the tool for automated unit test generation, which produces ready-to-use Java test cases with valid inputs. This year, it is implemented in two different variants: UTBot-fuzz that is a grey-box fuzzer and UTBot-concolic that has a dynamic symbolic execution engine in its core now paired with fuzzing. In this paper, we report the UTBot results at the SBFT 2023 Java tool competition.

In this work, we present a new benchmarking suite with new real-life inspired skewed workloads to test the performance of concurrent index data structures. We started this project to prepare workloads specifically for self-adjusting data structures, i.e., they handle more frequent requests faster, and, thus, should perform better than their standard counterparts. We looked over the commonly used suites to test performance of concurrent indices trying to find an inspiration: Synchrobench, Setbench, YCSB, and TPC - and we found several issues with them. The major problem is that they are not flexible: it is difficult to introduce new workloads, it is difficult to set the duration of the experiments, and it is difficult to change the parameters. We decided to solve this issue by presenting a new suite based on Synchrobench. Finally, we highlight the problem of measuring performance of data structures. We show that the relative performance of data structures highly depends on the workload: it is not clear which data structure is best. For that, we take three state-of-the-art concurrent binary search trees and run them on the workloads from our benchmarking suite. As a result, we get six experiments with all possible relative performance of the chosen data structures.

We present a solver for Java generics type system implemented using relational verifier-to-solver approach. The solver finds solutions for a system of subtyping inequations with free variables and thus can be used to determine a concrete type satisfying a set of constraints. The context of this work is symbolic execution for testing and verification of Java programs.

UTBotCpp and UTBot Java [3] are automatic white-box test generators for C/C++ and Java programs correspondingly. The tools were developed by Huawei and are based on symbolic and concrete execution. They try to cover as many branches as possible using program bytecode. For this purpose, UTBot tools analyze paths in the control flow graph of a given method, construct constraints for them, and try to find satisfying input values using SMT-solver to cover corresponding branches. In this paper, we report the results of UTBot Java at the tenth edition of the SBST 2022 tool competition.

UtBot is an automatic test generator for Java programs developed by Huawei and based on symbolic execution. It tries to cover as many branches as possible using the program's bytecode. To do that UtBot analyzes paths in the control flow graph of a given method, constructing constraints for them, and tries to find satisfying input values using SMT-solver to cover corresponding branches. In this paper, we report the results of UtBot at the ninth edition of the SBST 2021 tool competition.