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

All of us are crazy about mathematics and programming. We love taking part in software testingcompetitions and describe our achievements inresearch 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 consistentlyreplaced byTrue orFalse in such a way that the formula evaluates toTrue. 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 investigatebroader 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 supportsZ3 and Bitwuzla SAT solvers.

With SAT and SMT solvers, we develop symbolic execution technology to provide our precise code analysis andautomated 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 atSBST competitions.
• Our custom patch for KLEE is the core ofUnitTestBot C/C++. KLEE is a symbolic virtual machine built on top of the LLVM compiler infrastructure.Wecontribute to KLEE by implementing patches that enhance the engine’s codecoverage and speed. We offeredlazy initialization improvements and committed theundefined behavior detection patch as well as thepatch for inline assembly support to the main KLEE branch.We converted KLEE into thebidirectional property-directed symbolic execution engine. Moreover, the patched KLEE engine is able to automatically deduce method summaries.
• We also plan to support .NET infrastructure viaV# — the symbolic execution engine performing completely automated test generation for .NET assemblies.

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

While working on a UnitTestBot product lineup, we developfuzzing 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 theready-to-use tool forcode 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 theSoot 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 theJVM 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 togenerate human-readable test method bodies based on public API rather than Reflection.

We also develop thegenui project — a tool for automatic UI generation. Inour research, weelaborate ways to automaticallyarrange the elements of a user interface in accordance with the specified design guidelines. The next step is tosynthesize 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 tomake 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

Repositories