Johannes Hostert

Johannes Hostert is a Researcher at the Department of Computer Science (D-INFK), ETH Zurich, since October 2023. He works under the guidance of his advisor Ralf Jung in the PLF lab. His research focuses on program verification, separation logic, type theory, and formal methods in Rust programming.

• Bachelor’s and Master’s degrees from Saarland University
• Advisor: Ralf Jung

Research Trends include formal verification of programming languages, especially Rust and OCaml/C interoperability, mechanised logic in Coq, and aliasing models like Tree Borrows. His work bridges compiler optimization with memory safety guarantees.

Scientific Awards:

• Distinguished Paper Award for Tree Borrows (2025)

Labs & Collaborations: PLF lab at ETH Zurich, working with team members like Neven and Derek on projects such as Tree Borrows and MiniRust formalization.