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: CVC3 and IASolver. They use appropriate constraint solvers for complex math constraints and string operations.

They said, JPF-core has native peers mechanism to model native libraries and any other program part. It captures java.lang.Math libraries.

Sergey Vartanov, 2007–2020