2021-03-09 00:36:59 +00:00
|
|
|
**I will be moving to [Cornell University](https://www.cornell.edu) in Fall 2021.**
|
|
|
|
|
|
|
|
|
|
|
2019-10-28 02:33:14 +00:00
|
|
|
I am an assistant professor in the [Department of Computer
|
|
|
|
|
Sciences](https://www.cs.wisc.edu/) at the [University of
|
|
|
|
|
Wisconsin--Madison](https://www.wisc.edu).
|
2018-09-03 06:46:31 +00:00
|
|
|
|
|
|
|
|
|
2020-02-04 21:27:50 +00:00
|
|
|
**I am always looking for good students!**
|
2018-09-03 06:46:31 +00:00
|
|
|
|
|
|
|
|
|
2020-02-04 21:27:50 +00:00
|
|
|
Previously, I was a postdoc at the [Department of Computer
|
2018-03-24 23:49:19 +00:00
|
|
|
Science](https://www.cs.cornell.edu/) at [Cornell
|
2020-02-04 21:27:50 +00:00
|
|
|
University](https://www.cornell.edu/), and at the [Programming Principles,
|
2018-09-03 06:46:31 +00:00
|
|
|
Logic, and Verification Group](http://pplv.cs.ucl.ac.uk/welcome/) at the
|
2020-02-04 21:27:50 +00:00
|
|
|
[University College London](https://www.ucl.ac.uk/). I was a graduate student in
|
|
|
|
|
the [Department of Computer Science](https://cis.upenn.edu) at the [University
|
|
|
|
|
of Pennsylvania](https://www.upenn.edu).
|
2015-08-17 10:10:24 +00:00
|
|
|
|
2020-05-01 21:15:43 +00:00
|
|
|
I am funded by an NSF CAREER award and a Facebook Research award.
|
|
|
|
|
|
2015-01-05 04:43:45 +00:00
|
|
|
## Research Interests ##
|
2018-09-03 06:46:31 +00:00
|
|
|
I design methods to **formally verify** that programs are correct, especially
|
2018-09-03 06:47:05 +00:00
|
|
|
programs that use **randomization**. Such programs can be easy to show correct
|
|
|
|
|
on paper, but surprisingly challenging for computers to analyze. Accordingly,
|
|
|
|
|
my research blends ideas from two classical areas of computer science:
|
|
|
|
|
**randomized algorithms** from theoretical computer science (**TCS**) and
|
|
|
|
|
**formal verification**.
|
2018-09-03 06:46:31 +00:00
|
|
|
|
|
|
|
|
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**, and various notions of **algorithmic
|
|
|
|
|
stability**.
|
|
|
|
|
|
|
|
|
|
A particular focus of my work has been [**differential
|
2017-11-14 16:06:41 +00:00
|
|
|
privacy**](https://en.wikipedia.org/wiki/Differential_privacy), a rigorous
|
2015-01-05 04:43:45 +00:00
|
|
|
definition of privacy that is currently under extensive study.
|
2018-09-03 06:46:31 +00:00
|
|
|
I have investigated a variety of formal methods---such as [**type
|
2017-11-14 16:06:41 +00:00
|
|
|
systems**](https://en.wikipedia.org/wiki/Type_system) and [**program
|
|
|
|
|
logics**](https://en.wikipedia.org/wiki/Hoare_logic)---to verify that programs
|
2018-09-03 06:46:31 +00:00
|
|
|
are differentially private.
|
|
|
|
|
|
|
|
|
|
From a more traditional algorithms perspective, I am also interested in applying
|
|
|
|
|
differential privacy to optimization, machine learning, and mechanism design.
|
2017-01-17 10:33:57 +00:00
|
|
|
|
2018-09-05 03:51:09 +00:00
|
|
|
## Teaching ##
|
2021-07-10 22:35:42 +00:00
|
|
|
- **Reasoning about Probabilistic Programs (Invited Course, [OPLSS 2021](https://www.cs.uoregon.edu/research/summerschool/summer21/index.php))**:
|
|
|
|
|
[[slides](https://justinh.su/files/slides/oplss21.pdf)] [[recordings](https://www.cs.uoregon.edu/research/summerschool/summer21/topics.php)]
|
2021-01-14 23:01:45 +00:00
|
|
|
- **Security and Privacy in Data Science (CS 763)**: [F20](teaching/f20/cs763/)
|
2021-01-14 16:55:18 +00:00
|
|
|
- **Introduction to the Theory and Design of PL (CS 538)**: [S20](teaching/s20/cs538/)
|
|
|
|
|
- **Security and Privacy in Data Science (CS 763)**: [F19](teaching/f19/cs763/)
|
|
|
|
|
- **Introduction to the Theory and Design of PL (CS 538)**: [S19](teaching/s19/cs538/)
|
|
|
|
|
- **Topics in Security and Privacy Technologies (CS 839)**: [F18](teaching/f18/cs839/)
|
2018-09-05 03:51:09 +00:00
|
|
|
|
2017-01-17 10:33:57 +00:00
|
|
|
## Service ##
|
2021-07-10 22:36:18 +00:00
|
|
|
- **2022** POPL, PLDI
|
2021-04-01 22:14:17 +00:00
|
|
|
- **2021** ESOP, PLMW@POPL, CSF, AAAI, COLT, WoLLIC, MFPS
|
2020-05-18 17:24:05 +00:00
|
|
|
- **2020** AAAI, CSF, LAFI, WoLLIC, PLMW@POPL, OOPSLA (ERC)
|
2020-02-04 21:27:50 +00:00
|
|
|
- **2019** POPL, PLMW@POPL, POST, CSF, DARS (co-chair)
|
2018-05-25 20:37:57 +00:00
|
|
|
- **2018** LICS, WWW
|
|
|
|
|
- **2017** FCS, TPDP, MFPS
|
|
|
|
|
- **2016** PLDI (ERC)
|
