As software enters more aspects of society, including financial institutions, medical devices, and autonomous vehicles, ensuring the absence of software bugs becomes increasingly important. Symbolic execution engines are tools that allow automatically finding bugs via mathematical reasoning. Unfortunately, symbolic execution of certain programs can be slow to the point where it is entirely ineffective. This project develops techniques to improve efficiency, thus allowing symbolic execution to be applied to a wider range of software. The project's novelties are in identifying problematic code patterns which slow down symbolic execution and developing new techniques which improve efficiency of symbolic execution of this code. The project's impacts are that symbolic execution will become applicable to a greater range of programs in domains where correctness is critical- such as finance and medicine- reducing the risk of costly software failures. In addition to developing the proposed techniques, the investigator plans to develop and teach a Software Verification & Formal Methods course, incorporating research developed under this grant into the course material where appropriate. Further, both graduate and undergraduate students will work on this project, introducing them to research and formal methods techniques. Symbolic execution engines work by treating some program inputs as symbolic variables and "running" the program with these unknown values. When the program branch