I am a fourth year currently working with Olin Shivers and David Van Horn on higher-order flow analysis. I sometimes collaborate with Matt Might.

Generally, my work is on finding the right mathematical frameworks to concisely, correctly and easily define sound, precise and efficient flow analyses for modern programming languages. There are three (or four) dimensions of challenge for scaling such analyses.

  1. Efficiency
  2. Verifiability
  3. Precision
  4. (Grokability)

There is a promising approach to systematically and easily constructing provably sound and precise analyses by transforming abstract machines into abstract abstract machines, but the method lacks maturity. My work seeks to extend this method by importing innovations in both worlds of abstract machines (programming language interpreters) and unproven, but "works in practice" methods for improving analysis performance (or proven, but only for first-order languages). A primary constraint is maintaining the systematic and intuitive methods for derivation. The power is behind the intuitions, so a secondary goal in my work is to bring powerful analysis to a larger audience.



Combining intepreters and abstract interpreters:
Direct threading in bytecodes = abstract compilation.
JIT stack allocation = pushdown escape analysis with disposable stacks.

Generalizing and formalizing analyzers in "the wild":
SSA-based sparse analyses = trace inspection with fast-forwarding (ongoing)

The essence of summarization-based analysis:
Pushdown flow analysis for higher-order languages has two combating formalisms that are both unfortunately complex. There is a systematic approach to derive pushdown analyses that is simple and does not need expert knowledge on reachability queries for context-free languages to implement.

Correctly Optimizing Abstract Abstract Machines.
With David Van Horn, Matt Might and Nicholas Labich
[Abstract] [PDF]
Designing Precise Pushdown Higher-Order Flow Analyses. With David Van Horn
[Abstract]
Designing Precise Pushdown Higher-Order Flow Analyses. At IBM PL day 2012
[Slides]

Fundamentals of Computer Science 2 2510 (Summer 2012)

TA Office hours: Fridays 13:30-15:30
Location: WVH 308

Compilers 4410 (Spring 2012)

TA Office hours: By appointment
Location: WVH 308

Fundamentals of Computer Science 1 2500 (Fall 2011)

TA Office hours: Monday 10:00 - 12:00
Location: WVH 308

Fundamentals of Computer Science 2 2510 (Spring 2011)

Location: WVH 308

Program Design Paradigms 5010 (Fall 2010)

TA office hours: Friday 16:30 - 18:30
Location: WVH 308

Logic & Computation 2800 (Spring 2010)

TA office hours: Wednesday 9:30 - 10:30 and 12:30 - 13:30
Location: WVH 316

Logic & Computation 2800 (Fall 2009)

TA office hours: Tuesday 9:00 - 11:00
Location: WVH 316
Lab materials: Click here.
My interests are mostly in the realm of semantics and formal methods, dealing with flow analysis, interactive theorem proving and satisfiability modulo theories (SMT). I have done work with macros and binding specification. A pie in the sky very nice thing to see done would be a theorem prover built in the tower of languages style, with varying levels of abstraction as the tower grows, and an accompanying theory of how one reasons about macros. In my free time, I enjoy playing the piano and continuing my studies in algebra and combinatorics. I also speak Japanese and enjoy movies and video games. I cook and bake very tasty food.

I maintain a blog that is sporadically updated with theorems I find interesting, or how I have hacked around a sparsely documented or buggy API/application so that others may use the power of Google to solve their problems.

Valid XHTML 1.0 Strict