Kohler, EddieChong, StephenLu, Eric Hanqing2025-09-1820252025-01-172025Lu, Eric Hanqing. 2025. Efficient Symbolic Execution and Reasoning for Low Level Code. Doctoral Dissertation, Harvard University Graduate School of Arts and Sciences.31770274https://dash.harvard.edu/handle/1/42719421Systems should be correct, and automated reasoning promises to help construct correct systems. A common toolchain for automated reasoning about programs, used in program verification, program synthesis, and automated bug-finding, is symbolic execution and constraint solving. This dissertation describes the application and optimization of this toolchain in two projects. First, we discuss optimizing assembly program synthesis for OS porting with a deductive approach. Then, we introduce branch deferral, a way to optimize symbolic execution in bug-finding by reducing the number of paths explored when executing short-circuit control flow graphs.application/pdfenComputer scienceThesis or Dissertation2025-09-180000-0003-1228-9887