: Symbolic Execution of Java Bytecode
1 Combination of model checking and SE for error detection and test case generation. JPF-core executes program concretely (based on their custom VM), SPF performs symbolic interpretation. 2 Supported solvers: and . They use appropriate constraint solvers for complex math constraints and .
They said,has native peers mechanism to model native libraries and any other program part. It captures java.lang.Math libraries.
Sergey Vartanov, 2007–2020