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