diff --git a/talks/drodt.md b/talks/drodt.md index fe85218..6359ebd 100644 --- a/talks/drodt.md +++ b/talks/drodt.md @@ -8,4 +8,7 @@ slot: 113 order: 34 --- -TBD +For 25 years, the KeY tool has been used to verify the correctness of Java programs. We work toward generalizing KeY's approach and its codebase to new languages. The most ambitious such language is Rust, which ensures memory safety without a garbage collector. + +We present some compelling problems resulting from extending KeY to a new language, some unique properties of Rust, and their impact on verification. +