How to implement a symbolic execution engine for a particular language?

Question

I'm considering using symbolic execution to test the robustness of programs written in a particular language such as java. I've read some papers introducing the basic concepts of symbolic execution. But I'm not clear about how to get it started.

For example, how can I generate the constraint conditions from a concrete input? So any one can give me some advice on the basics of the implementation of symbolic execution? Furthermore, what about concolic execution(concrete + symbolic) ?

Answer 1

how can I generate the constraint conditions from a concrete input?

using symbolic or concolic execution

So any one can give me some advice on the basics of the implementation of symbolic execution?

My advice is the same as Ziming Zhao: use an existent symbolic execution tool. Do not attempt to implement your own, it would be too hard and time-consuming.

Here are the most popular projects (a more complete list here):

Java: JPF + Symbolic Pathfinder, JCute.

C and C++: KLEE, Kite