| Static program analysis can improve programmer productivity and software reliability by definitively ruling out entire classes of programmer mistakes. For mainstream imperative languages such as C, C++, and Java, static analysis about the heap---memory that is dynamically allocated at run time---is particularly challenging because heap memory acts as global, mutable state.;This dissertation describes how to soundly combine two static analyses that each take vastly different approaches to reasoning about the heap: type systems and separation logic. Traditional type systems take an alias-agnostic, global view of the heap that affords both fast verification and light-weight annotation of invariants holding over the entire program. Separation logic, in contrast, provides an alias-aware, local view of the heap in which invariants can vary at each program point.;In this work, I show how type systems and separation logic can be safely and efficiently combined. The result is type-intertwined separation logic, an analysis that applies traditional type-based reasoning to some regions of the program and separation logic to others---converting between analysis representations at region boundaries---and summarizes some portions of the heap with coarse type invariants and others with precise separation logic invariants.;The key challenge that this dissertation addresses is the communication and preservation of heap invariants between analyses. I tackle this challenge with two core contributions. The first is type-consistent summarization and materialization, which enables type-intertwined separation logic to both leverage and selectively violate the global type invariant. This mechanism allows the analysis to efficiently and precisely verify invariants that hold almost everywhere. Second, I describe gated separating conjunction, a non-commutative strengthening of standard separating conjunction that expresses local dis-pointing relationships between sub-heaps. Gated separation enables local heap reasoning by permitting the separation logic to frame out portions of memory and prevent the type system from interfering with its contents---an operation that would be unsound in type-intertwined analysis with only standard separating conjunction. With these two contributions, type-intertwined separation logic combines the benefits of both type-like global reasoning and separation-logic-style local reasoning in a single analysis. |
