I do not understand how symbolic execution is different from Whitebox fuzzing? From what I understand, Whitebox Fuzzers symbolically execute the code with some initial input format. Additionally, it will be helpful if someone could differentiate between these two forms with reference to KLEE and AFL tools.
Whitebox fuzzing can be done not only with symbolic execution. SAGE from Microsoft Research is an example of a whitebox fuzzer that uses concolic execution, also called dynamic symbolic execution, see NDSS08.
Yes, Whitebox Fuzzers get some seed/seeds (initial input/inputs) and symbolically execute the code with these. Concolic fuzzers also run the code with these inputs in parallel with symbolic execution.
KLEE is a whitebox fuzzer that uses symbolic execution.
AFL is a greybox fuzzer - it uses internal structure information only to calculate coverage and not to get new paths. There are tools for AFL that get constants from comparisions in the code and add these to AFLs dictionaries, but this is still not whitebox fuzzing.