I have transitioned to a new name, Dionna Amalie Glaze. Old publications are here under my old name for posterity only.
I have successfully defended my dissertation on automating the construction of higher-order program analyses. Many thanks to my advisor, David Van Horn, co-advisor, Olin Shivers, mentor and committee member, Mitch Wand, and external committee member, Cormac Flanagan.
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.
- Efficiency
- Verifiability
- Precision
- (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.
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.
Fundamentals of Computer Science 2 2510 (Summer 2012)
TA Office hours: Fridays 13:30-15:30Location: WVH 308
Compilers 4410 (Spring 2012)
TA Office hours: By appointmentLocation: WVH 308
Fundamentals of Computer Science 1 2500 (Fall 2011)
TA Office hours: Monday 10:00 - 12:00Location: WVH 308
Fundamentals of Computer Science 2 2510 (Spring 2011)
Location: WVH 308Program Design Paradigms 5010 (Fall 2010)
TA office hours: Friday 16:30 - 18:30Location: WVH 308
Logic & Computation 2800 (Spring 2010)
TA office hours: Wednesday 9:30 - 10:30 and 12:30 - 13:30Location: WVH 316
Logic & Computation 2800 (Fall 2009)
TA office hours: Tuesday 9:00 - 11:00Location: WVH 316
Lab materials: Click here.
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.