Cambridge PhD - 5 funded Positions via CASCADE & More

Stream: job postings

[Tobias Grosser]

Join me (https://grosser.science) on the quest to formalize the LLVM/MLIR ecosystem. I am looking for future PhD students with interests in Lean and formal methods. If you enjoy working on open-source and like to collaborate globally this position might be for you.

We have 5 funded positions via CASCADE (where we also invite Lean enthusiasts to apply). Cambridge additionally offers every year numerous fellowships which you are put forward to automatically.

Drop me a message on zulip in case this sparks your interest!

Apply before December 3rd to maximize your chance for funding.

Further information: https://grosser.science/#join

Some of the recent work we did:

• Lean
  • Automatic Translation of Authoritative RISCV Semantics (and others) to Lean: https://github.com/opencompl/sail-riscv-lean
  • Lean-MLIR (https://github.com/opencompl/lean-mlir)
  • Decision Procedures for Lean's BitVec
    • Certified Decision Procedures for Width-Independent Bitvector Predicates
    • Interactive Bitvector Reasoning using Verified Bit-Blasting - Henrik (Lean FRO) implemented bv_decide
• MLIR
  • First-Class Verification Dialects for MLIR
  • Hardware Design Automation at https://circt.llvm.org
  • ISA level Dialects

After having contributed to building some of the key foundations, we are now looking forward to bring more automated verification into the LLVM ecosystem.

Cambridge has a lively Lean and Formal Methods community, an excellent Tech Scene, is close to London for big city vibes, and otherwise. Our department host the SAIL is specification language (Peter Sewell, ...), the Cheri microarchitecture (Robert Watson, Simon Moore...), the opentitan root-of-trust (Rob Mullins via LowRisc), Isabelle (Larry Paulson). Our AI researchers in CARAMEL (https://caraml-group.github.io/) have various lines of work around Lean.