Publication: Efficient Symbolic Execution and Reasoning for Low Level Code
Loading...
Open/View Files
Date
2025-01-17
Authors
Published Version
Published Version
Journal Title
Journal ISSN
Volume Title
Publisher
The Harvard community has made this article openly available. Please share how this access benefits you.
Citation
Lu, Eric Hanqing. 2025. Efficient Symbolic Execution and Reasoning for Low Level Code. Doctoral Dissertation, Harvard University Graduate School of Arts and Sciences.
Abstract
Systems 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.
Description
Other Available Sources
Research Data
Keywords
Computer science
Terms of Use
This article is made available under the terms and conditions applicable to Other Posted Material (LAA), as set forth at Terms of Service