What is the application of symbolic execution? Do symbolic execution only generate path condition? How can I use symbolic execution to verify contract?
The most famous usage of symbolic execution is test input generation. For example, KLEE is a tool that generates test inputs for C programs using symbolic execution.
Another application would be assertion checking. If by contract you mean pre and post conditions, then yes, symbolic execution can also be used for that purpose.