Semantics-based Program Analysis via Symbolic Composition of Transfer Relations (Ph.D. Thesis) Christopher Colby The goal of program analysis is to determine automatically properties of the run-time behavior of a program. Tools of software development, such as compilers, program-verification systems, and program-comprehension systems, are in large part based on program analyses. Most semantics-based program analyses model the run-time behavior of a program as a trace of execution states and compute a property of these states. Typically, this property is drawn from a predetermined language of semantic information, such as aliasing descriptions or types of values. The standard methodology of program analysis is to construct the property as a fixed point, a single execution step at a time. We explain that these ubiquitous methodological choices---the a priori choice of the describable program properties and the use of a fixed-point computation---have some fundamental limitations and can result in poor precision. In this dissertation, we present a different approach to semantics-based program analysis. Our methodology is based on transfer relations that precisely describe the changes between the state of memory one point during execution and the state of memory at some later point in the execution. We isolate a language TR of concise computer-representable presentations of transfer relations. We also give an algorithm \oplus that, given two transfer relations from TR, symbolically constructs a third transfer relation in TR that is semantically equivalent to their relational composition. An analysis designed beings by describing the operational semantics of a source language as a set of TR-terms that precisely describe the atomic steps of execution. Then an analysis algorithm repeatedly applies \oplus to build a precise run-time description of any finite control path of interest. We show that TR is expressive enough to describe a wide variety of source-language features, including heap-allocated mutable data structures, arrays, pointers, and first-class functions. We then explain how our analysis methodology overcomes some current limitations of program analysis. The transfer relations themselves are useful program properties and would be difficult or impossible to formulate with classical approaches to program analysis. But we also describe some classes of analysis applications that are based on transfer relations. For instance, we explain that the classical limitation of program analysis to build a property a single execution step at a time can result in dramatic loss of precision, but may be overcome by using \oplus to compose multiple steps before applying a classical analysis. Furthermore, we show how to compute precise properties of loops symbolically, avoiding the inevitable imprecision of a fixed-point computation.