Semantics-Based Program Analysis via Symbolic Composition of Transfer Relations

iv 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-veri cation 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 xed 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 xed-point computation|have some fundamental limitations and can result in poor precision. In this dissertation, we present a dierent approach to semantics-based progra