Home

Prospective PhD Students

I am recruiting PhD students to begin in Fall 2027. Potential projects include:

  • Scalable Neurosymbolic Static Analysis: Augmenting efficient static analysis techniques with neural oracles to extend their expressivity without sacrificing performance.
  • Verification of Randomized Distributed Algorithms: Proving the correctness of critical algorithms, including blockchain consensus and secure multiparty computation schemes.
  • Interoperable Logics: Enabling specifications to be shared across large proof artifacts that span multi-million-line codebases.

Who should apply

Strong candidates will have a background in programming languages, for example coursework or research experience in programming language theory, type systems, program logics, formal verification, and/or proof assistants such as Rocq or Lean.

Some of my work intersects with AI, but it is grounded in the formal foundations that make verification trustworthy and efficient. I am not interested in projects that simply experiment with LLMs to verify programs in a freeform way. If that is your main interest, I am unlikely to be the right advisor for you.

If you meet these criteria, please reach out to me!

How to apply

See the Stevens Computer Science PhD program page for details on how to apply.