Computer Science Department
Carnegie Mellon University
My primary areas of interest are programming languages and software verification. I am looking for graduate students with strong backgrounds in 1) the formal aspects of programming languages (semantics; proofs) and 2) building realistic systems and tools. Students are not required to be strong in both, though I encourage students to have an interest in both. My application domains of focus are security/privacy and biological modeling, but I am open-minded about other application domains. Happy to talk to strong postdoctoral candidates and enthusiastic undergraduate students as well.
The School of Computer Science PhD application is here. The final deadline for 2017-2018 academic year is December 15, 2016.
Research projects of interest include, but are not limited to, the following.
Information leaks often occur because conditional access checks are intertwined with other functionality. I want to make software more secure by reducing opportunities for programmers to inadvertently leak information. My work on the Jeeves programming language introduced the idea of policy-agnostic programming: separating privacy and security policies from the rest of the code while relying on the compiler/compile to implement policy checks. Jeeves enforces policies at runtime. Follow-up work on Lifty uses a static program repair-based approach for inserting the necessary conditional checks at compile-time, where the programmer specifies policies as refinement types. I am interested in, among other things, the following extensions of this work:
Understanding the mechanisms behind cellular signalling would help us understand and cure many diseases, but the complexity of cellular signalling precludes understanding. I want to develop language constructs and programming tools for modeling cellular signalling as programs. My work on executable knowledge exploits a deep connection between programming language semantics and semantics to support a new way of modeling. We use Kappa, a rule-based graph-rewrite programming language that allows us to encode possible transformations over graphs representing the state of the cell. Kappa's precise operational semantics allow us to not only simulate the programs, but also perform static program analysis. We are currently working as part of the Big Mechanism project to mine models from the literature. Below are some project directions.
I have compiled the following advice on applying for a PhD in computer science:
If you are considering a stint in academia, you may also be interested in these blog posts I have written:
|Reasons to Pursue a Ph.D.||December 11, 2011|
|The Life of an Academic, Explained||February 5, 2012|
|How Science Really Works||January 12, 2013|
|What My PhD Was Like||February 27, 2016|