diff --git a/content/about.md b/content/about.md index 7eb136f..24fde69 100644 --- a/content/about.md +++ b/content/about.md @@ -21,7 +21,7 @@ and Facebook Research. ## Research Interests ## I design methods to **formally verify** that **algorithms** are correct. I am -especially interested in programs satisfying quantitative guarantees, or +especially interested in programs satisfying quantitative guarantees, or other properties from mathematical or scientific applications. A particular focus of my work has been verifying programs that use @@ -29,17 +29,12 @@ A particular focus of my work has been verifying programs that use surprisingly challenging for computers to analyze. Drawing inspiration from how humans reason about randomized algorithms, we can build simpler and more automated verification techniques. In the past, I've applied this approach to -properties like **accuracy**, **incentive compatibility**, Markov chain -**mixing**, various notions of **algorithmic stability**, and [**differential -privacy**](https://en.wikipedia.org/wiki/Differential_privacy), a rigorous -definition of privacy. I have developed a variety of [**type -systems**](https://en.wikipedia.org/wiki/Type_system) and [**program -logics**](https://en.wikipedia.org/wiki/Hoare_logic) to verify that programs are -differentially private. +properties like **statistical accuracy**, **incentive compatibility**, Markov +chain **mixing**, **algorithmic stability**, and **differential privacy**. -More broadly, I am interested in verifying all kinds of programs and properties -with rich mathematical structure, such as continuous-time systems, programs with -symmetries, economic mechanisms, and most recently, algorithms from numerical +More broadly, I am interested in verification for all kinds of programs with +rich mathematical structure and properties, such as continuous-time systems, +programs with symmetries, economic mechanisms, and algorithms from numerical analysis and applied mathematics. ## Teaching ##