just as the title,anyone knows the difference of the ways that those tool use to find bug? kLEE and SAGE maybe can find out-of-bound access and buffer overflow, KLEE can use assertions ,but any other ways?
Your question is very generic. I recommend reading the scientific papers and the documentation for an in-depth information.
However, SAGE mainly uses Concolic Execution, while KLEE uses (vanilla) Symbolic Execution. S2E is still distinct from these (even though being a distant KLEE fork) in that is uses dynamic switching between symbolic and concrete execution, using a jit that allows on-the-fly translation between QEMU-BC and LLVM-BC.
This pertains to the fundamental difference in the execution paradigm used by these particular tools, but clearly it can only scratch the surface.
For the end user one relevant distinction is that KLEE must be compiled with a particular compiler capable of emitting llvm code (eg. llvm-gcc or clang) and the developer must mess around with the build system. This usually means that KLEE is limited to plain C. S2E doesn't care which language you use and you can run compiled binaries, but the drawback is that some buffer-overruns cannot be detected and the execution is a bit slower (up to factor 100x). It depends on what you are trying to analyse.