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.
Sun 17 OctDisplayed time zone: Central Time (US & Canada) change
09:00 - 10:20 | |||
09:00 60mKeynote | Solidifying and Advancing the Software FoundationsVirtual Keynote Talks Zhendong Su ETH Zurich | ||
10:50 - 12:10 | Analysis / Synthesis Research Papers at Zurich D +8h Chair(s): Jiasi Shen Massachusetts Institute of Technology | ||
10:50 15mTalk | Scalable and Modular Robustness Analysis of Deep Neural NetworksVirtual Research Papers Yuyi Zhong School of Computing, National University of Singapore, Quang-Trung Ta National University of Singapore, Tianzuo Luo School of Computing, National University of Singapore, Fanlong ZHANG School of Computer, Guangdong University of Technology, Siau-Cheng Khoo National University of Singapore | ||
11:05 15mTalk | Server-Side Computation of Package Dependencies in Package-Management SystemsVirtual Research Papers | ||
11:20 10mTalk | PyCT: A Python Concolic TesterVirtual Research Papers Wei-Lun Tsai Academia Sinica, Wei-Cheng Wu University of Southern California, USA, Di-De Yen Academia Sinica, Fang Yu National Chengchi University, Yu-Fang Chen Academia Sinica, Taiwan | ||
11:30 10mTalk | Program Synthesis for Musicians: A Usability Testbed for Temporal Logic SpecificationsVirtual Research Papers Wonhyuk Choi Columbia University, Michel Vazirani Columbia University, Mark Santolucito Barnard College, Columbia University, USA | ||
11:40 10mTalk | Function Pointer Eliminator for C ProgramsVirtual Research Papers Daisuke Kimura Toho University , Mahmudul Faisal Al Ameen University of Tokyo, Makoto Tatsuta National Institute of Informatics, Koji Nakazawa Nagoya University | ||
11:50 20mLive Q&A | Q&A and discussionVirtual Research Papers | ||
13:50 - 15:10 | Compilation / TransformationResearch Papers at Zurich D +8h Chair(s): Sam Lindley The University of Edinburgh, UK | ||
13:50 15mTalk | A Dictionary-Passing Translation of Featherweight GoVirtual Research Papers Martin Sulzmann Karlsruhe University of Applied Sciences, Germany, Stefan Wehr Offenburg University of Applied Sciences | ||
14:05 15mTalk | A compilation method for dynamic typing in MLVirtual Research Papers | ||
14:20 15mTalk | Fully Abstract and Robust Compilation and How to Reconcile the Two, AbstractlyVirtual Research Papers Carmine Abate Max Planck Institute for Security and Privacy, Bochum, Germany, Matteo Busi Università di Pisa - Dipartimento di Informatica, Stelios Tsampas FAU Erlangen-Nuremberg, INF 8 | ||
14:35 15mTalk | Hybrid quantum-classical circuit simplification with the ZX-calculusVirtual Research Papers Agustín Borgna Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France and Université Paris-Saclay, CNRS, Laboratoire Méthodes Formelles, 91405, Orsay, France, Simon Perdrix Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay | ||
14:50 20mLive Q&A | Q&A and discussionVirtual Research Papers | ||
17:00 - 18:20 | |||
17:00 60mKeynote | Solidifying and Advancing the Software FoundationsVirtual Keynote Talks Zhendong Su ETH Zurich | ||
18:50 - 20:10 | |||
18:50 15mTalk | Scalable and Modular Robustness Analysis of Deep Neural NetworksVirtual Research Papers Yuyi Zhong School of Computing, National University of Singapore, Quang-Trung Ta National University of Singapore, Tianzuo Luo School of Computing, National University of Singapore, Fanlong ZHANG School of Computer, Guangdong University of Technology, Siau-Cheng Khoo National University of Singapore | ||
19:05 15mTalk | Server-Side Computation of Package Dependencies in Package-Management SystemsVirtual Research Papers | ||
19:20 10mTalk | PyCT: A Python Concolic TesterVirtual Research Papers Wei-Lun Tsai Academia Sinica, Wei-Cheng Wu University of Southern California, USA, Di-De Yen Academia Sinica, Fang Yu National Chengchi University, Yu-Fang Chen Academia Sinica, Taiwan | ||
19:30 10mTalk | Program Synthesis for Musicians: A Usability Testbed for Temporal Logic SpecificationsVirtual Research Papers Wonhyuk Choi Columbia University, Michel Vazirani Columbia University, Mark Santolucito Barnard College, Columbia University, USA | ||
19:40 10mTalk | Function Pointer Eliminator for C ProgramsVirtual Research Papers Daisuke Kimura Toho University , Mahmudul Faisal Al Ameen University of Tokyo, Makoto Tatsuta National Institute of Informatics, Koji Nakazawa Nagoya University | ||
19:50 20mLive Q&A | Q&A and discussionVirtual Research Papers | ||
21:50 - 23:10 | Compilation / Transformation (mirror)Research Papers at Zurich D Chair(s): Xin Zhang Peking University | ||
21:50 15mTalk | A Dictionary-Passing Translation of Featherweight GoVirtual Research Papers Martin Sulzmann Karlsruhe University of Applied Sciences, Germany, Stefan Wehr Offenburg University of Applied Sciences | ||
22:05 15mTalk | A compilation method for dynamic typing in MLVirtual Research Papers | ||
22:20 15mTalk | Fully Abstract and Robust Compilation and How to Reconcile the Two, AbstractlyVirtual Research Papers Carmine Abate Max Planck Institute for Security and Privacy, Bochum, Germany, Matteo Busi Università di Pisa - Dipartimento di Informatica, Stelios Tsampas FAU Erlangen-Nuremberg, INF 8 | ||
22:35 15mTalk | Hybrid quantum-classical circuit simplification with the ZX-calculusVirtual Research Papers Agustín Borgna Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France and Université Paris-Saclay, CNRS, Laboratoire Méthodes Formelles, 91405, Orsay, France, Simon Perdrix Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay | ||
22:50 20mLive Q&A | Q&A and discussionVirtual Research Papers | ||
Mon 18 OctDisplayed time zone: Central Time (US & Canada) change
09:00 - 10:20 | |||
09:00 60mKeynote | A Separation Logic for Probabilistic IndependenceVirtual Keynote Talks Justin Hsu University of Wisconsin-Madison, USA | ||
10:50 - 12:10 | |||
10:50 15mTalk | A Typed Programmatic Interface to Contracts on the BlockchainVirtual Research Papers | ||
11:05 15mTalk | Adaptable Traces for Program ExplanationsVirtual Research Papers Divya Bajaj Oregon State University, Martin Erwig Oregon State University, Danila Fedorin Oregon State University, Kai Gay Oregon State University | ||
11:20 15mTalk | Latent Effects for Reusable Language ComponentsVirtual Research Papers Birthe van den Berg KU Leuven, Casper Bach Poulsen Delft University of Technology, Tom Schrijvers KU Leuven, Nicolas Wu Imperial College London, UK | ||
11:35 15mTalk | The Choice Construct in the Soufflé LanguageVirtual Research Papers Xiaowen Hu The University of Sydney, Joshua Karp The University of Sydney, David Zhao The University of Sydney, Abdul Zreika The University of Sydney, Xi Wu The University of Sydney, Bernhard Scholz University of Sydney | ||
11:50 20mLive Q&A | Q&A and discussionVirtual Research Papers | ||
13:50 - 15:10 | |||
13:50 15mTalk | Preprocessing of Alternating Automata for Language Emptiness TestingVirtual Research Papers Pavol Vargovčík Brno University of Technology, Czech Republic, Lukáš Holík Brno University of Technology | ||
14:05 15mTalk | Proving LTL Properties of Bitvector Programs and Decompiled BinariesVirtual Research Papers Cyrus Liu Stevens Institute of Technology, Chengbin Pang Stevens Institute of Technology, Daniel Dietsch University of Freiburg, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Georgios Portokalidis Stevens Institute of Technology, Jun Xu Stevens Institute of Technology | ||
14:20 15mTalk | Solving Not-Substring with Flat AbstractionVirtual Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Lukáš Holík Brno University of Technology, Denghang Hu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Wei-Lun Tsai Academia Sinica, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Di-De Yen Academia Sinica | ||
14:35 15mTalk | Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program TerminationVirtual Research Papers Tsubasa Shoshi The University of Tokyo, Takuma Ishikawa The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan | ||
14:50 20mLive Q&A | Q&A and discussionVirtual Research Papers | ||
17:00 - 18:20 | |||
17:00 60mKeynote | A Separation Logic for Probabilistic IndependenceVirtual Keynote Talks Justin Hsu University of Wisconsin-Madison, USA | ||
18:50 - 20:10 | Language Design (mirror)Research Papers at Zurich D Chair(s): Andreea Costea School of Computing, National University Of Singapore | ||
18:50 15mTalk | A Typed Programmatic Interface to Contracts on the BlockchainVirtual Research Papers | ||
19:05 15mTalk | Adaptable Traces for Program ExplanationsVirtual Research Papers Divya Bajaj Oregon State University, Martin Erwig Oregon State University, Danila Fedorin Oregon State University, Kai Gay Oregon State University | ||
19:20 15mTalk | Latent Effects for Reusable Language ComponentsVirtual Research Papers Birthe van den Berg KU Leuven, Casper Bach Poulsen Delft University of Technology, Tom Schrijvers KU Leuven, Nicolas Wu Imperial College London, UK | ||
19:35 15mTalk | The Choice Construct in the Soufflé LanguageVirtual Research Papers Xiaowen Hu The University of Sydney, Joshua Karp The University of Sydney, David Zhao The University of Sydney, Abdul Zreika The University of Sydney, Xi Wu The University of Sydney, Bernhard Scholz University of Sydney | ||
19:50 20mLive Q&A | Q&A and discussionVirtual Research Papers | ||
21:50 - 23:10 | |||
21:50 15mTalk | Preprocessing of Alternating Automata for Language Emptiness TestingVirtual Research Papers Pavol Vargovčík Brno University of Technology, Czech Republic, Lukáš Holík Brno University of Technology | ||
22:05 15mTalk | Proving LTL Properties of Bitvector Programs and Decompiled BinariesVirtual Research Papers Cyrus Liu Stevens Institute of Technology, Chengbin Pang Stevens Institute of Technology, Daniel Dietsch University of Freiburg, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Georgios Portokalidis Stevens Institute of Technology, Jun Xu Stevens Institute of Technology | ||
22:20 15mTalk | Solving Not-Substring with Flat AbstractionVirtual Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Lukáš Holík Brno University of Technology, Denghang Hu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Wei-Lun Tsai Academia Sinica, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Di-De Yen Academia Sinica | ||
22:35 15mTalk | Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program TerminationVirtual Research Papers Tsubasa Shoshi The University of Tokyo, Takuma Ishikawa The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan | ||
22:50 20mLive Q&A | Q&A and discussionVirtual Research Papers | ||