Evan Chang
Assistant Professor of Computer Science at the University of Colorado Boulder
Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants
Abstract:
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.
Bio: Bor-Yuh Evan Chang (www.cs.colorado.edu/~bec/)
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.