I am ABD currently working with David Van Horn and Olin Shivers on higher-order program 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 program 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 construct 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.



Model-checking as contract checking:
Temporal contracts allow programmers to separately specify temporal properties their programs should satisfy by imposing a runtime monitor for enforcing these safety properties. Abstract interpretation of a language with temporal contracts is (sound) model-checking that language (ongoing)

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 = abstract self-adjusting computation (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.

My DBLP page
DLS 2014 Abstracting Abstract Control.
With David Van Horn. Journal of Functional Programming: Pushdown flow analysis with abstract garbage collection
With Ilya Sergey, Christopher Earl, Matt Might and David Van Horn. ICFP 2013: Optimizing Abstract Abstract Machines.
With David Van Horn, Matt Might and Nicholas Labich. HOPA 2013: Concrete Semantics for Pushdown Analysis: The Essence of Summarization.
With David Van Horn. Abstract presented at HOPA.
Designing Precise Pushdown Higher-Order Flow Analyses. With David Van Horn.
Abstracting Abstract Control At DLS 2014 Optimizing Abstract Abstract Machines At ICFP 2013 Concrete Semantics for Pushdown Analysis: The Essence of Summarization. At HOPA 2013 Designing Precise Pushdown Higher-Order Flow Analyses. At IBM PL day 2012 All sources to talks are available for education purposes on Github

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