We are a distributed team of researchers and engineers.

We are crazy about mathematics and programming. We love taking part in software testing competitions. We describe our achievements in research articles. We develop 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:

1. 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.

2. 
   

   SMT solving technology

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

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

3. 
   

   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.
     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.

   • We also plan to support .NET infrastructure via V# — the symbolic execution engine performing completely automated test generation for .NET assemblies.

4. 
   

   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.

5. 
   

   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 which 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.

6. 
   

   Program synthesis

   We investigate approaches to synthesizing code for solving practical problems.
   For example, UnitTestBot 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.

Though all these things may sound nerdy, we believe we develop a useful tool 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. And we welcome you to join us in developing UnitTestBot!

Contact us directly to ask a question, share your ideas or give us feedback — we will be glad to hear from you!

Visit our GitHub page and feel free to contribute!