JS Symbolic AnalyzerARKTS · TYPESCRIPT · USVM Read the thesis →
Symbolic execution engine

Run every path
your ArkTS code
could take.

A symbolic execution engine for ArkTS and TypeScript. It replaces concrete inputs with symbolic ones, collects a path constraint at every branch, and asks an SMT solver which paths are actually reachable — built on the USVM core.

See how it works Watch a function split →
symbolic value concrete value path constraint
execution treefindMinValue(arr: number[])
Concolic at the core

Concrete and symbolic, working together.

The engine keeps two representations of every value at once. Concrete values run the program forward like normal; symbolic values stand in for "any input" and accumulate the constraints that would make a path possible.

Concrete

The value you actually pass in

Pinning some variables to real values shrinks the search space and keeps the solver fast. When arr.length is known, the loop bound is known — no branching needed.

Symbolic

The value the solver gets to choose

A symbolic α represents every input at once. Each branch records a constraint on it; the SMT solver then decides which combinations are satisfiable and reports a concrete witness for each.

From source to reachable states

A four-stage pipeline.

Each stage hands a cleaner representation to the next — from human-readable ArkTS down to SMT formulas a solver can reason about.

01 — PARSE

ArkTS source

Your code, with its TypeScript type annotations recovered from the official grammar so argument types survive compilation.

▸ ANTLR · TypeScript grammar
02 — LOWER

Three-address code

The control-flow graph is lowered to a flat instruction set — loops, branches and try/catch made explicit and easy to walk.

▸ JacoDB · ArkTS IR
03 — INTERPRET

Symbolic interpreter

Each instruction steps the symbolic state, models implicit type coercion, and forks a new state at every reachable branch.

▸ USVM · PandaMachine
04 — SOLVE

SMT decision

Path constraints become SMT formulas. The solver discards unsatisfiable paths and returns a concrete input for every state that remains.

▸ KSMT · SMT solver
What the interpreter supports

Built for the awkward parts of the language.

The hard cases in ArkTS and TypeScript aren't the arithmetic — they're dynamic typing, loops without explicit jumps, and exception flow. Those are modeled directly.

Concolic execution

Mix concrete and symbolic values to cut the state space without losing coverage.

Bidirectional search

Explore paths forward and backward to reach a target state with the right inputs.

TypeScript type model

Argument types are parsed back from source and fed into the constraints as bounds.

Implicit coercion

All sixteen pairs of number · bool · string · object handled via nested ite.

Loops without jumps

Cycles are recovered from the basic-block graph, with phantom gotos pruned away.

Nested try / catch

A traversal-strategy stack models exception scopes, including catches inside catches.

One function, four states

Watch a function split.

Feed in findMinValue with a symbolic array. The engine walks every reachable path and reports the input that triggers each one.

findMinValue.ts
function findMinValue(arr: number[]): number {
  if (arr.length === 0)
    throw new Error("Array is empty!");

  let minValue = arr[0];
  for (let i = 1; i < arr.length; i++) {
    if (arr[i] < minValue) {
      minValue = arr[i];
    }
  }
  return minValue;
}
State 1terminal · exception
pc: len(α) = 0
result: throw "Array is empty!"
State 2min at index 0
pc: len(α) > 0 ∧ ∀i>0 · α[i] ≥ α[0]
result: return α[0]
State 3+min discovered later
pc: len(α) > 0 ∧ ∃k · α[k] < α[0]
result: return min(α)

Each state carries its inputs, its path, and its result — enough to flag dead code or generate a covering unit test.

Research origin

From a bachelor's thesis to a working engine.

This engine grew out of a graduation project at Saint Petersburg State University: extending the USVM symbolic-analysis core with a full ArkTS interpreter, plus the JacoDB changes needed to make it run.

USVM on GitHub JacoDB →