Thibaut Pérami

I'm a French computer science PhD student, at the university of Cambridge, supervised by Peter Sewell.

My current research

Formal hardware modeling   I'm working on expanding and improving hardware architecture models for the ARM architecture, especially system feature such as virtual memory in the context of concurrent accesses.

Mechanized Formalisation of architecture models   I'm also working on implementing usable a definition of those models in the Coq proof assistant to enable formal verification using those models.

Long term goals   I want to be able to verify complicated and concurrent system software without assuming correct any snippets of assembly code like most previous projects in system verification did. I also want myself or more likely other programmers to be able to write system programs without being afraid of Heisenbugs due to concurency in edge-cases, even for complicated systems code.

My interests

  • System/Bare metal programming. So far most of my experience is with x86_64 and ARM, but I'm also interested by RISC-V.
  • Concurrency and GPU programming: how to make efficient concurrent programs with low overhead.
  • Low-level safety and security, how to avoid memory safety issue and various other low-level pitfalls.
  • Programming language design
    • especially features related to the first three points
    • I'm also generally interested in meta-programing/generic programming/dependent typing in system languages (such as C++ templates and Rust generics and traits).
  • Compiler design and implementation, where I'm interested in performance but as importantly correctness, especially related to low-level concurrency and memory accesses.
  • Formal verification of system software with concurrency and low-level memory pattern, but also compiler verification.
  • Formal modeling of hardware architectures to help write correct system code and enable its formal verification
  • I'm also interested in proof automation as it helps greatly formal verification effort, especially:
    • SMT solving
    • automated proof search procedure in proof assistant

Mail

I can be contacted by mail at my University of Cambridge address: thibaut.perami AT cl.cam.ac.uk.