## [GlassTT] A Symbolic Java Virtual Machine for Test Case Generation

symbolic virtual machine

1 See also *Babel Abstract Machine* and *Warren Abstract Machine*. Their symbolic execution is based on user-specified coverage criterion. And they focus on *def-use-chain criterion* (to cover as many def-use chains as possible). Def-use: from one variable definition to value destruction. Def-use-chain: from one definition to many destructions. 2 They do only *few* iterations of each loop. GlassTT is SJVM and it itself implemented in Java and run on JVM. Facepalm. They simplify (*x* + 1 + 1) to (*x* + 2) on-the-fly. Expressions are object tree in the host JVM's heap.

3 They implement stack and heap, full JVM specification, backtracking mechanism, exception table. 4 They treat exceptions and danger instructions like conditional jumps. In fact, they *are* conditional jumps. They use SA to discover def-use chains. Coverage criteria: (1) def-use chains, (2) branch coverage, (3) instruction. 5 They use Mathematica as a solver.

So, I think, they perform SE for one method, not for entire program.

7 pages

See also their paperConstraint Solving for Generating Glass-Box Test Casesabout solving optimization. They do solving before SMT-solvers.

Sergey Vartanov, 2007–2020