Skip to content
@UnitTestBot

UnitTestBot

Welcome, friends! 👋

We are a distributed team of researchers and engineers 🙋‍.

All of us are crazy about mathematics and programming. We love taking part in software testing competitions and describe our achievements in research articles.

The main project we share is our flagship product — UnitTestBot for Java/Kotlin, C/C++, Python, JavaScript, and Go.

To be in touch with the high-end science, we collaborate with the top-rated universities. As a part of the intercollegiate team, we develop root technologies to empower UnitTestBot as well as the whole lineup of other software products. Here are some of them:

🤓 SAT solving technology

SAT solver is a computer program asking whether the variables of a given Boolean formula can be consistently replaced by True or False in such a way that the formula evaluates to True. SAT solvers are frequently used as the “engine” for the program verification applications.

  • KoSAT is a pure Kotlin CDCL SAT solver based on MiniSat core. It solves Boolean satisfiability problems given in DIMACS format and supports incremental solving.
  • We also investigate broader theoretical questions related to SAT solving, e.g. evaluating the computational hardness of a given SAT problem.

🧐 SMT solving technology

Satisfiability modulo theories (SMT) field of research relates to determining whether a logic formula is satisfiable.

KSMT is the Java/Kotlin facade for various SMT solvers. For now, it supports Z3 and Bitwuzla SAT solvers.

😎 Symbolic execution

With SAT and SMT solvers, we develop symbolic execution technology to provide our precise code analysis and automated test generation tools with the effective engines. We have three main solutions in this research area.

  • UnitTestBot Java has its own dynamic symbolic execution engine that has already shown excellent results at SBST competitions.
  • Our custom patch for KLEE is the core of UnitTestBot C/C++. KLEE is a symbolic virtual machine built on top of the LLVM compiler infrastructure. We contribute to KLEE by implementing patches that enhance the engine’s code coverage and speed. We offered lazy initialization improvements and committed the undefined behavior detection patch as well as the patch for inline assembly support to the main KLEE branch. We converted KLEE into the bidirectional property-directed symbolic execution engine. Moreover, the patched KLEE engine is able to automatically deduce method summaries.
  • We also plan to support .NET infrastructure via V# — the symbolic execution engine performing completely automated test generation for .NET assemblies.

Symbolic execution is the main focus of our interest, so we conducted a series of research related to both applied and fundamental problems in this field.

🤪 Fuzzing

While working on a UnitTestBot product lineup, we develop fuzzing and dynamic program analysis techniques suitable for all supported languages: Java/Kotlin, C/C++, Python. JavaScript, and Go.

🙂 Program analysis

UnitTestBot with its symbolic execution engine and fuzzing techniques is the ready-to-use tool for code analysis. In addition to this end-to-end solution, we implement a basic framework for developing custom static code analyzers.

Java Compilation Database (JacoDB) was inspired by the Soot framework for analyzing and transforming Java code.

JacoDB is a pure Java database that stores information about the compiled Java bytecode — classes, hierarchies, annotations, methods, fields, and their usages. With JacoDB, it is possible to analyze bytecode located outside the JVM process. It allows UnitTestBot to support the newest JDKs and to reuse data between restarts.

🙃 Program synthesis

We investigate approaches to synthesizing code for solving practical problems. For example, UnitTestBot is able to generate human-readable test method bodies based on public API rather than Reflection.

We also develop the genui project — a tool for automatic UI generation. In our research, we elaborate ways to automatically arrange the elements of a user interface in accordance with the specified design guidelines. The next step is to synthesize the code that is capable of implementing this layout.

Stay tuned 🧙

Though all these things may sound nerdy, we believe we develop useful tools for real-life programmers. We try to make UnitTestBot effective and user-friendly — so that we are happy with it when we use it ourselves.

Feel free to join us in developing UnitTestBot! ✌

BTW, you can check our friends: https://github.com/program-analysis-team

Pinned Loading

  1. UTBotCpp UTBotCpp Public

    Tool that generates unit test by C/C++ source code, trying to reach all branches and maximize code coverage

    C++ 159 27

  2. UTBotJava UTBotJava Public

    Automated unit test generation and precise code analysis for Java

    Kotlin 137 45

  3. jacodb jacodb Public

    fast and effective way to access and analyze java bytecode

    Kotlin 23 16

  4. klee klee Public

    Forked from klee/klee

    KLEEF Symbolic Execution Engine

    C++ 14 11

  5. kosat kosat Public

    Pure Kotlin CDCL SAT solver

    Kotlin 7 1

  6. ksmt ksmt Public

    Kotlin/Java API for various SMT solvers

    Kotlin 30 15

Repositories

Showing 10 of 30 repositories
  • usvm Public

    Universal Symbolic Virtual Machine

    UnitTestBot/usvm’s past year of commit activity
    Kotlin 23 Apache-2.0 21 35 4 Updated Dec 24, 2024
  • jacodb Public

    fast and effective way to access and analyze java bytecode

    UnitTestBot/jacodb’s past year of commit activity
    Kotlin 23 Apache-2.0 16 21 9 Updated Dec 21, 2024
  • klee Public Forked from klee/klee

    KLEEF Symbolic Execution Engine

    UnitTestBot/klee’s past year of commit activity
    C++ 14 696 11 (1 issue needs help) 11 Updated Dec 9, 2024
  • UTBotCpp Public

    Tool that generates unit test by C/C++ source code, trying to reach all branches and maximize code coverage

    UnitTestBot/UTBotCpp’s past year of commit activity
    C++ 159 Apache-2.0 27 118 (2 issues need help) 3 Updated Oct 18, 2024
  • ksmt Public

    Kotlin/Java API for various SMT solvers

    UnitTestBot/ksmt’s past year of commit activity
    Kotlin 30 Apache-2.0 15 5 7 Updated Oct 18, 2024
  • UnitTestBot/java-stdlib-approximations’s past year of commit activity
    Java 0 6 8 2 Updated Aug 13, 2024
  • msbuild-database Public

    An MsBuild logger that emit compile_commands.json and link_commands.json files from a C++ project build.

    UnitTestBot/msbuild-database’s past year of commit activity
    C# 1 MIT 2 0 0 Updated Jul 16, 2024
  • UTBotJava Public

    Automated unit test generation and precise code analysis for Java

    UnitTestBot/UTBotJava’s past year of commit activity
    Kotlin 137 Apache-2.0 45 386 30 Updated Jun 3, 2024
  • UTBotPythonSBFT2024 Public

    UTBot-Python-SBFT-Competitions-2024

    UnitTestBot/UTBotPythonSBFT2024’s past year of commit activity
    Python 1 Apache-2.0 0 0 0 Updated May 23, 2024
  • utbotc_tests Public
    UnitTestBot/utbotc_tests’s past year of commit activity
    C 0 0 0 0 Updated Apr 22, 2024