Dissertation/Thesis Abstract

Type-Intertwined Separation Logic
by Coughlin, Devin, Ph.D., University of Colorado at Boulder, 2015, 203; 3704668
Abstract (Summary)

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.

Indexing (document details)
Advisor: Chang, Bor-Yuh Evan
Commitee: Diwan, Amer, Jhala, Ranjit, Sankaranarayanan, Sriram, Siek, Jeremy G.
School: University of Colorado at Boulder
Department: Computer Science
School Location: United States -- Colorado
Source: DAI-B 76/10(E), Dissertation Abstracts International
Subjects: Computer science
Keywords: Dependent types, Objective-c, Separation logic, Type systems
Publication Number: 3704668
ISBN: 9781321772579
Copyright © 2019 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy