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 paper Constraint Solving for Generating Glass-Box Test Cases about solving optimization. They do solving before SMT-solvers.

Sergey Vartanov, 2007–2020