I am broadly interested in the principles and practice of programming languages, and applications of logic in computer science. I am an expert in formal, mechanized methods for reasoning about programs, including abstract interpretation, model checking, and deductive verification. More recently, I have developed an interest in the design of languages and systems for parallel and multicore programming. My current research projects are listed below.
[Wordle Word cloud generated from recent talks and abstracts.]
Cauchy: towards an analytical calculus of computation
The Cauchy project aims to build an "analytical calculus of computation": a system of mechanized reasoning that can verify whether a program satisfies "analytic" properties like continuity and smoothness, and compute derivatives, discontinuities, limits, and other analytic attributes of programs. The practical motivation of the project is to develop a new class of program analyses for an era where computing is intertwined with sensor-derived perceptions of the physical world, and correctness is a continuum rather than a boolean fact. The desktop application of yesterday that runs on the cyber-physical system of today is still written in a standard language allowing branches, loops, queues, and arrays, and must still satisfy traditional safety and liveness properties. However, as it now processes real-valued, real-time satellite and sensor data, it must also offer a new set of analytic guarantees. For example, we may now require that the program be "robust" to small amounts of uncertainty in its inputs—i.e., that small perturbations to an input state only lead to small changes to the output state. A way to formalize this statement would be to define a metric space over the states of the program, and ask that the program encode a continuous function over this space. Alternately, we may consider the derivative of the program as a measure of its robustness, insisting that a program with a smaller derivative is more robust. To tune program parameters, we may want to use classical root-finding techniques, which may only work on an analytic approximation of the program. To argue that a program converges, we may want to compute limits on its outputs as time elapses to infinity. Common to the above scenarios is the need for some form of analytic reasoning about programs.
The scope of Cauchy includes the theoretical foundations of such reasoning, ways to automate it using state-of-the-art constraint-solvers and numerical optimizers, and its applications in program verification, synthesis, optimization, and approximation. In the recently-published first paper out of this project, we have given a method to automatically verify that a program represents a continuous function. In a subsequent paper, we give a method to compute smooth approximations of programs and apply it to program synthesis. From evidence so far, Cauchy opens a new playground for research on reasoning about programs. It also raises the possibility of a fruitful union of program semantics and verification with control theory, numerical analysis, machine learning, and computer algebra.
Chorus: dynamic isolation in shared-memory parallelism
Chorus is a new programming model for parallel computations manipulating complex shared-memory data structures. The primary concern of Chorus is to express fine-grained, isolated, concurrent accesses to the heap, in settings where the amount of isolation needed depends on the instance and changes dynamically. The main abstraction of the model is an object assembly: a local region in the shared heap equipped with a thread of control. At any point during an execution of a Chorus program, numerous assemblies execute concurrently. However, these assemblies are always non-overlapping, so that objects within them are isolated. Assemblies grow and shrink at runtime by "merging" with each other and "splitting" into smaller assemblies, chainging the granularity of isolation dynamically. The programmer defines the behavior of a program's assemblies through a set of "assembly classes," which generalize classes in object-oriented programming.
Chorus bridges a traditional gap between popular shared-memory programming models, which do not provide first-class abstractions for isolation and locality, and Actor-based parallel programming, which naturally captures locality but is unsuitable for computations on complex shared data structures. The model is particularly well-suited to programming irregularly data-parallel applications like Delaunay triangulation and clustering (the Lonestar benchmark suite contains several other applications of this class), which exhibit fine-grained data-parallelism in typical executions but almost no parallelism in the worst case, and have long been known to be important but difficult to parallelize.
In current work, we are using some of the ideas from Chorus to build a more general abstraction for weak isolation that is integrated with traditional abstractions for spatial locality and directed synchronization. This abstraction will be integrated with the Habanero Java language from Rice University. We are also developing a foundational process calculus capturing the essence of Chorus.
A prototype implementation of JChorus, an integration of Chorus and Java, is available here.
Procedure-modular program verification
Modular reasoning about software has long been a subject of interest to program verification. In particular, much recent work has studied approaches to program verification that exploit the procedural modularity of programs. My Ph.D. work studied the logical and algorithmic foundations of procedure-modular verification, and some of my current work continues on this theme.
Of particular interest to me are the theories of nested words and nested trees, which augment the traditional word and tree models used in program verification with an additional hierarchical structure, and can be used to model infinite behaviors of procedural, reactive programs. Logics and automata on these structures have robust theoretical properties, and lead to elegant yet tractable reasoning about procedural programs. My Ph.D. thesis developed and applied the theory of nested structures in the context of software model checking, an algorithmic approach to software analysis. My current work extends some of those ideas to general program verification. In addition, I am interested in algorithmic questions about modular verification, in particular parallelizing and distributing modular analysis of programs.