Zhendong Su, ETH Zurich

Title: Solidifying and Advancing the Software Foundations

Abstract

Software applications and technologies are built on top of foundational systems such as compilers, databases, and theorem provers. Such foundations form the trusted computing base, and fundamentally impact software quality and security. Thus, it is a critical challenge to solidify and advance them. This talk highlights general, effective techniques, and extensive, impactful efforts on finding hundreds of critical issues in widely-used compilers, database management systems, and SMT solvers. It focuses on the high-level principles and core techniques, their significant practical successes, and future opportunities and challenges.

Biography

Zhendong Su is a Professor in Computer Science at ETH Zurich. Previously, he was a Professor and Chancellor’s Fellow at UC Davis. He received his PhD in Computer Science from UC Berkeley. His research spans programming languages and compilers, software engineering, computer security, deep learning and education technologies. His work was recognized by an ACM SIGSOFT Impact Paper Award, a Google Scholar Classic Paper Award, multiple best/distinguished paper/artifact awards at top venues (e.g., PLDI, OSDI, OOPSLA, and ICSE), an ACM CACM Research Highlight, an NSF CAREER Award, a UC Davis Outstanding Faculty Award, and multiple industrial faculty awards (e.g., Cisco, Google, IBM, Microsoft, and Mozilla). He served on the steering committees of ISSTA and ESEC/FSE, served as an Associate Editor for ACM TOSEM, co-chaired SAS 2009, program chaired ISSTA 2012, and program co-chaired SIGSOFT FSE 2016. He is an elected member of the Academia Europaea.

Justin Hsu, Cornell University

Title: A Separation Logic for Probabilistic Independence

Abstract

Probabilistic independence is a useful concept for describing the result of random sampling—a basic operation in all probabilistic languages—and for reasoning about groups of random variables. Nevertheless, existing verification methods handle independence poorly, if at all. We propose a probabilistic separation logic PSL, where separation models probabilistic independence, based on a new, probabilistic model of the logic of bunched implications (BI). The program logic PSL is capable of verifying information-theoretic security of cryptographic constructions for several well-known tasks, including private information retrieval, oblivious transfer, secure multi-party addition, and simple oblivious RAM, while reasoning purely in terms of independence and uniformity. If time permits, we will also discuss ongoing work for reasoning about conditional independence.

Biography

Justin Hsu is an assistant professor of Computer Science at Cornell University. He was previously an assistant professor at UW–Madison and a postdoc at Cornell and UCL, after receiving his doctorate in Computer Science from the University of Pennsylvania. His research focuses on formal verification of probabilistic programs, including algorithms from differential privacy, protocols from cryptography, and mechanisms from game theory. His work has been recognized by an NSF CAREER award, a SIGPLAN John C. Reynolds Doctoral Dissertation award, a Facebook TAV award, a Facebook Probability and Programming award.