SHF: Small: Optimizing runtime efficiency of symbolic execution for functional languages

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 branches based on a symbolic variable, the symbolic executor splits into multiple states, and tracks the requirements for each state to execute. This project improves symbolic execution's efficiency by developing techniques to condense the number of program states that symbolic execution is required to reason about and reduce the amount of work required to reason about each individual state. The project is developing theory to allow showing correctness of the proposed techniques, in the sense that the optimizations do not risk symbolic execution missing any program failures. The optimizations are being practically implemented in an existing symbolic execution engine, G2, allowing an empirical evaluation of their effectiveness. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.