This is a survey of symbolic execution with an emphasis on the KLEE verifier. It is probably a better introduction to the concepts of symbolic execution than the baldoni:compsurv:2018 survey but this makes it less complete.
Like baldoni:compsurv:2018, this article describes some of the important optimizations to make symbolic execution effective including
Path optimizations such as random exploration, interleaving symbolic execution with random exploration, pruning redundant paths, lazy test generation (only exploring functions if their output is important to the constraint), static path merging (aka branch predication).
Constraint optimizations such as irrelevant constraint elimination, incremental solving (e.g., counterexample caching),