On Improving Backwards Reasoning with Symbolic Execution: Integrating Loop Summarization, Alias Analysis, and Compositional Summarization

Program analysis techniques play a crucial role in modern software development by helping developers find bugs and verify code behavior. These techniques rely heavily on systematic reasoning about program execution paths. Symbolic execution has emerged as a powerful method for systematic program analysis. However, symbolic execution faces a fundamental challenge known as state-space explosion, where the number of potential execution paths grows exponentially. While backwards symbolic execution (BSE) offers some advantages over forward approaches in managing this explosion, it still struggles with path explosion when handling complex program elements such as loops, pointers, and function calls. This dissertation advances backwards reasoning through several key contributions. We introduce BROIL, an approach that enables handling of loops in backwards reasoning without requiring complete loop unrolling. By developing parameterized loop summaries that capture loop behavior, BROIL significantly reduces the state-space explosion problem common in symbolic execution. We demonstrate BROIL's effectiveness by applying it with incorrectness logic for targeted assertions. Our empirical evaluation then investigates the question of which alias analysis technique best complements BSE. Through experimentation comparing different alias analysis approaches, we demonstrate that demand-driven analysis substantially outperforms whole-program approaches, achieving a 7.29× geometric mean speedup in symbolic execution. Finally, we develop CAMS, a compositional approach for function summarization in backwards analysis. CAMS introduces context-agnostic function summaries that capture pointer and global variable effects while supporting modular composition. By enabling the reuse of summaries across different program units, CAMS achieves significant performance improvements compared to non-compositional approach.