Abstract Symbolic execution is a systematic technique for checking programs, which forms a basis for various software testing and verification techniques. It provides a powerful analysis in principle but remains challenging to scale and generalize symbolic execution in practice. This chapter reviews the cutting-edge research accomplishments in addressing these challenges in the last 5 years, including advances in addressing the scalability challenges such as constraint solving and path explosion, as well as advances in applying symbolic execution in testing, security, and probabilistic program analysis.