From b9e09bc6c289a4fb5cdcf71d5cb46e0bf4cc9484 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 21 Mar 2024 19:53:05 +0100 Subject: [PATCH 1/1] update website --- research/index.html | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/research/index.html b/research/index.html index d335f56..bd7b174 100644 --- a/research/index.html +++ b/research/index.html @@ -17,10 +17,13 @@ Please explain why you are interested in a PhD in this field and what your prior Note that doing a PhD at ETH Zürich generally requires a Master's degree, but there is a direct doctorate program that you can enter with a Bachelor's degree (application deadline December 15th).

-->

My two main lines of work are about Rust and Iris.
-On the Rust side, I am working (also in collaboration with the Rust language team) towards a solid formal foundation for the language, including in particular the unsafe parts. -One key result here is our type safety proof, which also describes a methodology for establishing type safety of well-encapsulated unsafe code. -My goal is to make unsafe Rust just as safe as safe Rust by means of formal verification.
-On the Iris side, besides continuing development of its logical foundations, I am interested in applying Iris to new problem domains; recently I started working on modular verification of fault-tolerant distributed system components.
+On the Rust side, me and my group are working (also in collaboration with the Rust language team) towards a solid formal foundation for the language, including in particular the unsafe parts. +As part of this we are developing Miri, a practical tool for detecting Undefined Behavior bugs in unsafe Rust code, which has become a part of the standard toolbox of unsafe code authors. +Meanwhile, MiniRust is our work-in-progress proposal for a precise specification of unsafe Rust, that I hope to integrate into an official Rust specification eventually. +My long-term goal is to make unsafe Rust just as safe as safe Rust by means of formal verification based on rigorous foundations for all key components of the language.
+On the Iris side, I am continuing development of its logical foundations. +We are making Iris fit for specifying and verifying programming languages at scale using a more modular approach. +The long-term goal is for Iris to be able to handle the full scale of complexities that arise when doing foundational verification of real languages.
For some more information, check out my research blog, my CV, and my research statement.

In my free time, I like to run internet services myself and work on free software. -- 2.30.2