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. / Doctor of Philosophy / Modern software has become increasingly complex, making it challenging for developers to ensure their code works correctly. To help with this, developers use program analysis tools that systematically check code for bugs. One promising approach is symbolic execution, which explores how a program behaves in different program paths. However, this approach struggles because the number of possible program states it needs to check grows too quickly. An approach, backwards symbolic execution, helps manage this problem by working backwards from potential bugs, but it still faces state-space explosion when analyzing common programming constructs like loops and function calls. This dissertation presents three solutions to make program analysis more practical. First, we introduce BROIL, a new approach that efficiently handles program loops by creating summaries of their behavior instead of analyzing them completely. We show how BROIL can be used effectively to find bugs in programs. Second, we investigate how different alias analysis techniques perform when integrated with backwards symbolic execution. Our experiments show that demand-driven alias analysis significantly outperforms traditional whole-program analysis approaches, achieving more than seven times speedup. Finally, we develop CAMS, a technique that creates reusable summaries of program functions. These summaries can be used across different parts of the program, making the analysis significantly faster than traditional approaches. Together, these contributions make program analysis tools more practical for analyzing real-world programs.