For this usually CBMC is used. http://www.cprover.org/cbmc/

You can also use CBMC to solve the usual state reverse engineering problems, like coverage analysis, finding input for output, hash collisions, ...