jFuzz is an automatic test generation tool which utilizes concolic (concrete and symbolic) execution to create new input files that execute different paths through the subject program.
jFuzz executes a given subject program and input file using the concolic bytecodes. These, like the bytecodes used in symbc, generate a PathCondition as the program executes. They also preserve the actual values which were used during execution, unlike symbc.
After execution is finished jFuzz systematically negates each conjunct in the PathCondition, creating a new PathCondition per conjunct. Then each of these new PathConditions are sent to a solver which creates the set of variables which would cause this new path to be taken. jFuzz then outputs a file which, on a subsequent run, will cause that path through the program to be executed.