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

Type of tool

Symbolic executor

Expected input


Expected output

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


License: Apache License v2.0
Binary level Java


Repository: https://github.com/SymbolicPathFinder/jpf-symbc

Related papers

Last publication date

4 April 2019

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.