What is the difference between symbolic execution and model checking (for example in model transformation)? I don't understand difference of them. Are they the same?!
In model checking, you have to encode your system as a Finite State Machine and provide that FSM to the model checker as well as a specification. The model checker will then make sure that the specification always holds in that system.
In symbolic execution you only provide your program and the symbolic execution engine will examine all the feasible paths to generate test inputs or check assertions.
A simple example of their difference: concurrency. Model checking can handle multi-thread systems because it is specified in the FSM provided as input, however, symbolic execution cannot handle more than one thread.