PV3 ⊧ SPF: Symbolic PathFinderchecks properties of annotated Java code with static symbolic execution

Symbolic Pathfinder (SPF) is a program analysis tool for Java bytecode; the tool is based on symbolic execution

Application domain/field

• Symbolic execution
• Model checking
• Automated test case generation

Type of tool

Symbolic executor

Expected input

• Java bytecode program
• Configuration file specifying, e.g. which methods should be executed symbolically

Format:

• Java bytecode program: .class
• Configuration file: .jpf

Expected output

Test suite (test inputs or test sequences) and/or counterexamples for the failed properties

Comments

License: Apache License v2.0