PV3 ⊧ Java Rangerchecks properties of annotated Java code with static symbolic execution
an extension of Symbolic PathFinder for veritesting and summarising dynamically dispatched methods and exceptional control-flow.Application domain/field
Symbolic executionType of tool
Symbolic execution toolExpected input
- Java code
- Configurations for the analysis
Format:
- Classpath: classpath of target code, given as an argument when calling Java Ranger
- Configurations, all arguments when calling Java Ranger:
veritestingMode = <1-5>indicating which path-merging features should be enabledperformanceMode = <true or false>jitAnalysis = <true or false>recursiveDepth = <integer value>