Computer Science Department
Carnegie Mellon University
Erin Davis, eedavis [at] andrew [dot] cmu [dot] edu
Our group mission is to take over the entire world with sound reasoning and provable guarantees. 🌈
Towards this mission, we are looking for graduate students with strong backgrounds in 1) the formal aspects of programming languages and 2) building realistic systems and tools. Students are not required to be strong in both, though it would be good to have an interest in both. I am happy to talk to strong postdoctoral candidates and enthusiastic undergraduate students as well.
You may read more about our research group and active projects here.
CMU has a large and active Principles of Programming group. The group has become even larger and more active now that Jan Hoffmann, Matt Fredrikson, and I have joined. The School of Computer Science PhD application is here.
Research projects include, but are not limited to, the following.
Information leaks often occur because conditional access checks are intertwined with other functionality. We want to make software more secure by reducing opportunities for programmers to inadvertently leak information. Our prior 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. We are 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. We are interested in developing language constructs and programming tools for modeling cellular signalling as programs. Our 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 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|
Pittsburgh is not just affordable and liveable, but also newly hip 🔥. Why wouldn't you want to be here?
|Pittsburgh Gets a Tech Makeover||July 22, 2017|
|A Revitalized Pittsburgh Suggests the President Used a Rusty Metaphor||June 2, 2017|
|Built on Steel, Pittsburgh Now Thrives on Culture||April 12, 2017|
|36 Hours in Pittsburgh||July 15, 2015|