Symbolic Testing

COYOTE is a fully automated unit testing tool that automatically creates test cases for each function of software and automatically executes their testing.

When you try to implement fully automatic testing, the most difficult part is the automatic creation of test cases. Although diverse techniques have been devised for scores of years, there have been many stumbles along the way.

Even though many test automation tools are advertised to be able to generate automatically test cases, they have been shunned away due to falling short of expectation.

With our own symbolic testing technology, we have developed a brand-new concolic execution engine which satisfies a new level of expectation for automatic generation of test cases. The symbolic testing technology performs white box testing using symbolic execution or concolic execution techniques and it exerts outstanding capabilities for automatic generation of test cases.

The symbolic testing engine explores all execution paths of a given function and calculates the conditions under which each execution path is executed (path condition).

For this it inserts some code into the given function to perform symbolic operations for symbolic conditions, and writes automatically driver code to call the function and stub code of callee functions called by that function. When running the test, the actual execution and the symbolic execution are performed simultaneously, and the symbolic execution calculates the path conditions and test cases. At the time, to solve the conditional equations, an automatic theorem prover such as an SMT solver is used.

Automatic Verification Team

“We develop a fully automated unit testing tool by combining technologies such as concolic execution, automatic proving, static analysis, machine learning, and more.”
“We enjoy functional programming and our main language is F#. If you like to work with functional lagnuages, contact us.”
“Source code analysis, SMT solving, and code generation play necessary roles in many parts of automated testing, as well as the symbolic testing technology.”
“We will do our utmost to be a reliable partner in industries where software reliability is particularly important, such as automotive and aviation.”

Static Analysis

CODEMIND CSI/CQI, a Static Application Security Testing Tool, detects security weaknesses inherent in the source code and finds possible runtime errors in advance.

The technology that predicts software’s behavior beforehand without execution of the software is so-called static analysis. Static analysis can be presented in a variety of techniques, including type analysis, data flow analysis, control flow analysis, information flow analysis, value analysis and memory shape analysis.

The abstract interpretation technology is for designing various static analysis techniques within one framework. It has established itself as a standard of the static analysis as it can systematically implement various semantic analyses based on abstract semantics.

The principle of the abstract interpretation is to compute abstracted values through abstracted operations of a given program. For example, the following simultaneous equation system can calculate an intervel value that each position’s x value can have with the given simple program. The solution of the simultaneous equation is called the “fixed point,” and the fixed point is calculated with a repetitive method.

In this way, variable values are computed, or memory allocation configuration is predicted. The second example is about the process of calculating the memory shape with the given program through abstract interpretation. The example illustrates detecting a use-after-free error with memory shape analysis.

Besides, CODEMIND has implemented a static analysis engine using graph DB. The analysis result can be checked during analysis in an on-the-fly style, and it is also useful for creating convenient defect tracking graphs.

Static Analysis Team

“We develop static analysis tools based on abstract interpretation. We provide security testing and quality testing using syntax analysis, flow analysis, memory analysis, and value analysis.”
“We are programming in functional languages and objective-oriencted languages such as Scala and Java.”
“We have integrated graph DB-based analysis and semantic-based analysis to implement on-the-fly analysis and provide defect tracking graphs.
“Since each customer presents different development environments and analysis requirements recently, offering proper customization becomes important. We will do our best to meet customer needs on application security testing.”