中央研究院 資訊科學研究所

We present a generic analysis approach to the imperative relationship update problem, in which destructive updates temporarily violate a global invariant of interest.  Such invariants can be conveniently and concisely specified with dependent refinement types, which are efficient to check flow-insensitively. Unfortunately, while traditional flow-insensitive type checking is fast, it is inapplicable when the desired invariants can be temporarily broken.  While most prior approaches have ratcheted up the complexity of the type analysis and associated type invariant, we propose a generic lifting of modular refinement type analyses with a symbolic analysis to efficiently and effectively check concise invariants that hold almost everywhere.  The result is an efficient, highly modular flow-insensitive type analysis to optimistically check the preservation of global relationship invariants that can fall back to a precise, disjunctive symbolic analysis when the optimistic assumption is violated.  A significant challenge is selectively violating the global type consistency invariant over heap locations, which we achieve via almost type-consistent heaps.  To evaluate our approach, we have encoded the problem of verifying the safety of reflective method calls in dynamic languages as a refinement type checking problem.  Our analysis is capable of validating reflective call safety at interactive speeds on commonly-used Objective-C libraries and applications.

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.