Aarhus University Seal

talk by Bor-Yuh Evan Chang, U. Colorado Boulder

Type-Intertwined Heap Analysis

Monday, 18 May 11:00, Nygaard-295

Type-Intertwined Heap Analysis

We consider the problem of intertwining global, flow-insensitive type checking with local, symbolic, separation logic-based program analysis. Type-intertwined heap analysis combines the benefits of flow-insensitive, alias-agnostic type invariants---checking speed and low annotation burden---with precise path-sensitive, alias-aware symbolic reasoning about the heap. The key challenge in this work is the communication and preservation of heap invariants between these two analyses that take a dramatically different view of the heap. To tackle this challenge, we consider two core ideas. First, we discuss type-consistent materialization and summarization, which enables the intertwined analysis to both leverage and selectively violate the global type invariant. Second, we consider gated separating conjunction, a non-commutative strengthening of standard separating conjunction, to express local "dis-pointing" relationships between sub-heaps. Such dis-pointing relationships expressed by gated separation enables a frame rule for soundly applying type checking on a sub-heap. The benefit of type-intertwined static analysis is a gradual approach to the static checking of dynamic language programs---type checking is applied for the sub-heap that adheres to a static type system and symbolic program analysis is applied to the sub-heap that makes use of the flexibility of dynamic languages.

Biography:

Bor-Yuh Evan Chang is an Assistant Professor of Computer Science at the University of Colorado Boulder.  He is interested in tools and techniques for building, understanding, and ensuring reliable computational systems.  His techniques target using novel ways of interacting with the programmer to design more precise and practical program analyses.  He is a recipient of an NSF CAREER award.  He received his M.S. and Ph.D. from the University of California Berkeley and his B.S. from Carnegie Mellon University.