Check out the Java Pathfinder (from NASA, however, and for free). I think he should do what you need almost out of the box, i.e. Try different hooks (some assembly may be required).
Of course, you still need to specify the property of checking for your data that you are interested in, for example, an invariant. Otherwise, by default, you will probably only say if there was a dead end. Take a look at the “Explore Performance Alternatives” section.
source share