What every C Programmer should know about undefined behavior #2/3

Correct me if I'm wrong, but symbolic execution engines are what you get when you don't allow the halting problem to dissuade you from analyzing the code, and KLEE is a symbolic execution engine that generates test cases for interesting paths that it has deduced, such as paths to a bug. If a program is small enough KLEE can find many paths which result in the termination of the program, but for large applications KLEE can run for hours or days. In fact, it could run forever, AFAIU, if its heuristics don't terminate the algorithm. This is why it allows you to specify different starting points so you can get complete coverage over more interesting sub-components of an application.