justhsu
/
justin-site
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Shorter.

This commit is contained in:
Justin Hsu 2024-07-19 01:15:51 -04:00
parent 227d5ee393
commit 5787795f5c
1 changed files with 6 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
content/about.md
View File

@ -21,7 +21,7 @@ and Facebook Research.
## Research Interests ## ## Research Interests ##
I design methods to **formally verify** that **algorithms** are correct. I am 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. properties from mathematical or scientific applications.
A particular focus of my work has been verifying programs that use 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 surprisingly challenging for computers to analyze. Drawing inspiration from how
humans reason about randomized algorithms, we can build simpler and more humans reason about randomized algorithms, we can build simpler and more
automated verification techniques. In the past, I've applied this approach to automated verification techniques. In the past, I've applied this approach to
properties like **accuracy**, **incentive compatibility**, Markov chain properties like **statistical accuracy**, **incentive compatibility**, Markov
**mixing**, various notions of **algorithmic stability**, and [**differential chain **mixing**, **algorithmic stability**, and **differential privacy**.
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.
More broadly, I am interested in verifying all kinds of programs and properties More broadly, I am interested in verification for all kinds of programs with
with rich mathematical structure, such as continuous-time systems, programs with rich mathematical structure and properties, such as continuous-time systems,
symmetries, economic mechanisms, and most recently, algorithms from numerical programs with symmetries, economic mechanisms, and algorithms from numerical
analysis and applied mathematics. analysis and applied mathematics.
## Teaching ## ## Teaching ##