Justin Hsu

Contacts

Wisconsin
CS 6379
Madison, Wisconsin

Email
email@justinh.su

About Me

I am an assistant professor of Computer Science at the University of Wisconsin–Madison.

I am currently looking for good students!

Previously, I was a postdoc in the Department of Computer Science at Cornell University, hosted by Nate Foster, Bobby Kleinberg, and Dexter Kozen, and in the Programming Principles, Logic, and Verification Group at the University College London, hosted by Alexandra Silva. I was a graduate student in the Department of Computer Science at the University of Pennsylvania, where I was very fortunate to be advised by Benjamin Pierce and Aaron Roth.

Research Interests

I design methods to formally verify that programs are correct, especially 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.

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 privacy, a rigorous definition of privacy that is currently under extensive study. I have investigated a variety of formal methods—such as type systems and program logics—to verify that programs are differentially private.

From a more traditional algorithms perspective, I am also interested in applying differential privacy to optimization, machine learning, and mechanism design.

Teaching

  • Topics in Security and Privacy Technologies (CS 839): F18
  • Introduction to the Theory and Design of PL (CS 538): S19

Service

  • 2019 POPL, PLMW, POST, CSF, DARS (co-chair)
  • 2018 LICS, WWW
  • 2017 FCS, TPDP, MFPS
  • 2016 PLDI (ERC)
News
Bibliography

Drafts

2018
Metric Semantics for Probabilistic Relational Reasoning
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata.
[Paper]
2018
Probabilistic Program Equivalence for NetKAT
Steffen Smolka, Praveen Kumar, Nate Foster, Justin Hsu, David Kahn, Dexter Kozen, and Alexandra Silva.
[Paper]
2018
Approximate Span Liftings
Tetsuya Sato, Gilles Barthe, Marco Gaboradi, Justin Hsu, and Shin-ya Katsumata.
[Paper]

Thesis

2017
Probabilistic Couplings for Probabilistic Reasoning
Justin Hsu.
University of Pennsylvania.
[Paper]
Selected for the ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award

Refereed Publications

2019
Trace Abstraction modulo Probability
Calvin Smith, Justin Hsu, and Aws Albarghouthi.
Proceedings of the ACM on Programming Languages, 3(POPL).
[Paper]
To appear at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Lisbon, Portugal.
2019
Formal Verification of Higher-Order Probabilistic Programs
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu.
Proceedings of the ACM on Programming Languages, 3(POPL).
[Paper]
To appear at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Lisbon, Portugal.
2018
Convex Language Semantics for Nondeterministic Probabilistic Automata
Gerco van Heerdt, Justin Hsu, Joël Ouaknine, and Alexandra Silva.
In International Colloquium on Theoretical Aspects of Computing (ICTAC), Stellenbosch, South Africa.
[Paper]
2018
Constraint-Based Synthesis of Coupling Proofs
Aws Albarghouthi and Justin Hsu.
In International Conference on Computer Aided Verification (CAV), Oxford, England.
[Paper]
2018
Almost Sure Productivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, and Alexandra Silva.
In International Colloquium on Automata, Languages and Programming (ICALP), Prague, Czech Republic.
[Paper]
2018
An Assertion-Based Program Logic for Probabilistic Programs
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In European Symposium on Programming (ESOP), Thessaloniki, Greece.
[Paper] [Slides]
2018
Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi and Justin Hsu.
Proceedings of the ACM on Programming Languages, 2(POPL).
[Paper]
Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Los Angeles, California.
2018
Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
Proceedings of the ACM on Programming Languages, 2(POPL).
[Paper] [Slides]
Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Los Angeles, California.
2017
Dual Query: Practical Private Query Release for High Dimensional Data
Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Zhiwei Steven Wu.
Journal of Privacy and Confidentiality, 7(2).
[Paper] [Poster]
Previously published in International Conference on Machine Learning (ICML), Beijing, China, 2014.
2017
-Liftings for Differential Privacy
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub.
In International Colloquium on Automata, Languages and Programming (ICALP), Warsaw, Poland.
[Paper] [Slides]
2017
Proving Uniformity and Independence by Self-Composition and Coupling
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Maun, Botswana.
[Paper] [Slides]
2017
Coupling Proofs Are Probabilistic Product Programs
Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France.
[Paper] [Slides]
2017
A Semantic Account of Metric Preservation
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui.
In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France.
[Paper]
2016
Private Matchings and Allocations
Justin Hsu, Zhiyi Huang, Aaron Roth, Tim Roughgarden, and Zhiwei Steven Wu.
SIAM Journal on Computing, 45(6).
[Paper] [Poster]
Previously published in ACM SIGACT Symposium on Theory of Computing (STOC), New York, New York, 2014.
2016
Computer-Aided Verification in Mechanism Design
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub.
In Conference on Web and Internet Economics (WINE), Montréal, Québec.
[Paper] [Slides]
2016
Advanced Probabilistic Couplings for Differential Privacy
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In ACM SIGSAC Conference on Computer and Communications Security (CCS), Vienna, Austria.
[Paper] [Slides]
There is an error in the treatment of advanced composition; please see my thesis for the correction.
2016
Differentially Private Bayesian Programming
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, and Pierre-Yves Strub.
In ACM SIGSAC Conference on Computer and Communications Security (CCS), Vienna, Austria.
[Paper]
2016
Synthesizing Probabilistic Invariants via Doob’s Decomposition
Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu.
In International Conference on Computer Aided Verification (CAV), Toronto, Ontario.
[Paper]
2016
A Program Logic for Union Bounds
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In International Colloquium on Automata, Languages and Programming (ICALP), Rome, Italy.
[Paper]
2016
Proving Differential Privacy via Probabilistic Couplings
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In IEEE Symposium on Logic in Computer Science (LICS), New York, New York.
[Paper] [Slides]
2016
Do Prices Coordinate Markets?
Justin Hsu, Jamie Morgenstern, Ryan Rogers, Aaron Roth, and Rakesh Vohra.
In ACM SIGACT Symposium on Theory of Computing (STOC), Cambridge, Massachusetts.
[Paper]
2016
Jointly Private Convex Programming
Justin Hsu, Zhiyi Huang, Aaron Roth, and Zhiwei Steven Wu.
In ACM–SIAM Symposium on Discrete Algorithms (SODA), Arlington, Virginia.
[Paper] [Slides]
2016
Programming Language Techniques for Differential Privacy
Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce.
ACM SIGLOG News, 3(1).
[Paper]
2015
Relational Reasoning via Probabilistic Coupling
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub.
In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Suva, Fiji.
[Paper] [Slides]
2015
Online Assignment with Heterogeneous Tasks in Crowdsourcing Markets
Sepehr Assadi, Justin Hsu, and Shahin Jabbari.
In AAAI Conference on Human Computation and Crowdsourcing (HCOMP), San Diego, California.
[Paper]
2015
A Theory AB Toolbox
Marco Gaboardi and Justin Hsu.
In Summit on Advances in Programming Languages (SNAPL), Asilomar, California.
[Paper] [Slides]
2015
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub.
In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India.
[Paper] [Slides]
2015
Death, Taxes, and Formal Verification (Abstract)
Justin Hsu.
In Summit on Advances in Programming Languages (SNAPL), Asilomar, California.
[Paper] [Slides]
2014
Really Natural Linear Indexed Type-Checking
Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu.
In Symposium on Implementation and Application of Functional Programming Languages (IFL), Boston, Massachusetts.
[Paper] [Slides]
2014
Proving Differential Privacy in Hoare Logic
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub.
In IEEE Computer Security Foundations Symposium (CSF), Vienna, Austria.
[Paper]
2014
Differential Privacy: An Economic Method for Choosing Epsilon
Justin Hsu, Marco Gaboardi, Andreas Haeberlen, Sanjeev Khanna, Arjun Narayan, Benjamin C. Pierce, and Aaron Roth.
In IEEE Computer Security Foundations Symposium (CSF), Vienna, Austria.
[Paper] [Slides]
2014
Privately Solving Linear Programs
Justin Hsu, Aaron Roth, Tim Roughgarden, and Jonathan Ullman.
In International Colloquium on Automata, Languages and Programming (ICALP), Copenhagen, Denmark.
[Paper] [Slides]
2013
System FC with Explicit Kind Equality
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), Boston, Massachusetts.
[Paper]
2013
Differential Privacy for the Analyst via Private Equilibrium Computation
Justin Hsu, Aaron Roth, and Jonathan Ullman.
In ACM SIGACT Symposium on Theory of Computing (STOC), Palo Alto, California.
[Paper] [Slides]
2013
Linear Dependent Types for Differential Privacy
Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce.
In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy.
[Paper]
2013
Automatic Sensitivity Analysis using Linear Dependent Types
Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, Justin Hsu, and Benjamin C. Pierce.
In International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA), informal proceedings.
[Paper]
2012
Distributed Private Heavy Hitters
Justin Hsu, Sanjeev Khanna, and Aaron Roth.
In International Colloquium on Automata, Languages and Programming (ICALP), Warwick, England.
[Paper] [Slides]
Thanks to Raef Bassily and Adam Smith for spotting an error, now fixed.