The problem of input crafting can be stated as follows: given the ability to influence some aspect of a program's execution (say, by supplying it with a hand-crafted file, network input, sequence of keystrokes, etc), we want to know whether it is possible to cause the program to reach some state, for example, a condition where the integer argument to some memory allocation function is zero, a specific sequence of branches being taken causing EIP to obtain a certain value, an array dereference whose index is not within its bounds, etc. Much work in reverse engineering for vulnerability analysis and software cracking reduces to this problem; some malware analysis problems can also be stated in such terms.

It is well-known in the formal verification literature that symbolic execution, a method for reasoning about program executions based upon formal semantics and theorem proving, may be applied towards this problem. However, actual tools that can be used in a friendly fashion have not yet materialized in the hands of the common, working reverse engineer. This blog entry demonstrates a prototype of a tool of this nature.

Crafting inputs with manually-generated SMT instances
This is by far, another great blog entry by Rolf Rolles and something i feel is an area which we should or could be looking at.
Please do read his article and the video which he made to have a better understanding of it.

The link to the original article is here:
http://www.openrce.org/blog/view/2049/[video]_Semi-Automated_Input_Crafting_by_Symbolic_Execution,_with_an_Application_to_Automatic_Key_Generator_Gener ation

BR,
[ Gunther ]