APLAS 2021 - Keynote Talks - APLAS 2021

APLAS 2021 - Keynote Talks - APLAS 2021
Write a Blog >>
APLAS 2021
Sun 17 - Fri 22 October 2021
Chicago, Illinois, United States
co-located with
SPLASH 2021
Attending
Venue: Swissotel Chicago
Program
APLAS Program
Your Program
Sun 17 Oct
Mon 18 Oct
Tue 19 Oct
Wed 20 Oct
Thu 21 Oct
Fri 22 Oct
Tracks
APLAS 2021
Keynote Talks
Research Papers
Organization
APLAS 2021 Committees
Track Committees
Organising Committee
Program Committee
Contributors
People Index
Series
Series
APLAS & ATVA 2026
APLAS 2025
APLAS 2024
APLAS 2023
APLAS 2022
APLAS 2021
APLAS 2020
APLAS 2019
SPLASH 2021
series
) /
APLAS 2021
series
) /
Keynote Talks
APLAS 2021
About
Program
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.
Dates
Tracks
Program Display Configuration
Close
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 17 Oct
Displayed time zone:
Central Time (US & Canada)
change
09:00 - 10:20
Invited talk 1
Keynote Talks
at
Zurich D
+8h
Chair(s):
Hakjoo Oh
Korea University
09:00
60m
Keynote
Solidifying and Advancing the Software Foundations
Virtual
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
15m
Talk
Scalable and Modular Robustness Analysis of Deep Neural Networks
Virtual
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
15m
Talk
Server-Side Computation of Package Dependencies in Package-Management Systems
Virtual
Research Papers
Nobuhiro Kasai
Shibaura Institute of Technology
Isao Sasano
Shibaura Institute of Technology
11:20
10m
Talk
PyCT: A Python Concolic Tester
Virtual
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
10m
Talk
Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications
Virtual
Research Papers
Wonhyuk Choi
Columbia University
Michel Vazirani
Columbia University
Mark Santolucito
Barnard College, Columbia University, USA
11:40
10m
Talk
Function Pointer Eliminator for C Programs
Virtual
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
20m
Live Q&A
Q&A and discussion
Virtual
Research Papers
13:50 - 15:10
Compilation / Transformation
Research Papers
at
Zurich D
+8h
Chair(s):
Sam Lindley
The University of Edinburgh, UK
13:50
15m
Talk
A Dictionary-Passing Translation of Featherweight Go
Virtual
Research Papers
Martin Sulzmann
Karlsruhe University of Applied Sciences, Germany
Stefan Wehr
Offenburg University of Applied Sciences
14:05
15m
Talk
A compilation method for dynamic typing in ML
Virtual
Research Papers
Atsushi Ohori
Tohoku University, Japan
Katsuhiro Ueno
Tohoku University
14:20
15m
Talk
Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
Virtual
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
15m
Talk
Hybrid quantum-classical circuit simplification with the ZX-calculus
Virtual
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
20m
Live Q&A
Q&A and discussion
Virtual
Research Papers
17:00 - 18:20
Invited talk 1
Keynote Talks
at
Zurich D
Chair(s):
Xinyu Wang
University of Michigan
17:00
60m
Keynote
Solidifying and Advancing the Software Foundations
Virtual
Keynote Talks
Zhendong Su
ETH Zurich
18:50 - 20:10
Analysis / Synthesis (mirror)
Research Papers
at
Zurich D
Chair(s):
Kihong Heo
KAIST
18:50
15m
Talk
Scalable and Modular Robustness Analysis of Deep Neural Networks
Virtual
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
15m
Talk
Server-Side Computation of Package Dependencies in Package-Management Systems
Virtual
Research Papers
Nobuhiro Kasai
Shibaura Institute of Technology
Isao Sasano
Shibaura Institute of Technology
19:20
10m
Talk
PyCT: A Python Concolic Tester
Virtual
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
10m
Talk
Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications
Virtual
Research Papers
Wonhyuk Choi
Columbia University
Michel Vazirani
Columbia University
Mark Santolucito
Barnard College, Columbia University, USA
19:40
10m
Talk
Function Pointer Eliminator for C Programs
Virtual
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
20m
Live Q&A
Q&A and discussion
Virtual
Research Papers
21:50 - 23:10
Compilation / Transformation (mirror)
Research Papers
at
Zurich D
Chair(s):
Xin Zhang
Peking University
21:50
15m
Talk
A Dictionary-Passing Translation of Featherweight Go
Virtual
Research Papers
Martin Sulzmann
Karlsruhe University of Applied Sciences, Germany
Stefan Wehr
Offenburg University of Applied Sciences
22:05
15m
Talk
A compilation method for dynamic typing in ML
Virtual
Research Papers
Atsushi Ohori
Tohoku University, Japan
Katsuhiro Ueno
Tohoku University
22:20
15m
Talk
Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
Virtual
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
15m
Talk
Hybrid quantum-classical circuit simplification with the ZX-calculus
Virtual
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
20m
Live Q&A
Q&A and discussion
Virtual
Research Papers
Mon 18 Oct
Displayed time zone:
Central Time (US & Canada)
change
09:00 - 10:20
Invited talk 2
Keynote Talks
at
Zurich D
+8h
Chair(s):
Atsushi Igarashi
Kyoto University, Japan
09:00
60m
Keynote
A Separation Logic for Probabilistic Independence
Virtual
Keynote Talks
Justin Hsu
University of Wisconsin-Madison, USA
10:50 - 12:10
Language Design
Research Papers
at
Zurich D
+8h
Chair(s):
Sergio Mover
Ecole Polytechnique
10:50
15m
Talk
A Typed Programmatic Interface to Contracts on the Blockchain
Virtual
Research Papers
Thi Thu Ha Doan
University of Freiburg
Peter Thiemann
University of Freiburg, Germany
11:05
15m
Talk
Adaptable Traces for Program Explanations
Virtual
Research Papers
Divya Bajaj
Oregon State University
Martin Erwig
Oregon State University
Danila Fedorin
Oregon State University
Kai Gay
Oregon State University
11:20
15m
Talk
Latent Effects for Reusable Language Components
Virtual
Research Papers
Birthe van den Berg
KU Leuven
Casper Bach
Delft University of Technology
Tom Schrijvers
KU Leuven
Nicolas Wu
Imperial College London, UK
11:35
15m
Talk
The Choice Construct in the Soufflé Language
Virtual
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
20m
Live Q&A
Q&A and discussion
Virtual
Research Papers
13:50 - 15:10
Verification / Theory
Research Papers
at
Zurich D
+8h
Chair(s):
Xiaokang Qiu
Purdue University, USA
13:50
15m
Talk
Preprocessing of Alternating Automata for Language Emptiness Testing
Virtual
Research Papers
Pavol Vargovčík
Brno University of Technology, Czech Republic
Lukáš Holík
Brno University of Technology
14:05
15m
Talk
Proving LTL Properties of Bitvector Programs and Decompiled Binaries
Virtual
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
15m
Talk
Solving Not-Substring with Flat Abstraction
Virtual
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
15m
Talk
Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program Termination
Virtual
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
20m
Live Q&A
Q&A and discussion
Virtual
Research Papers
17:00 - 18:20
Invited talk 2
Keynote Talks
at
Zurich D
Chair(s):
Xujie Si
McGill University, Canada
17:00
60m
Keynote
A Separation Logic for Probabilistic Independence
Virtual
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
15m
Talk
A Typed Programmatic Interface to Contracts on the Blockchain
Virtual
Research Papers
Thi Thu Ha Doan
University of Freiburg
Peter Thiemann
University of Freiburg, Germany
19:05
15m
Talk
Adaptable Traces for Program Explanations
Virtual
Research Papers
Divya Bajaj
Oregon State University
Martin Erwig
Oregon State University
Danila Fedorin
Oregon State University
Kai Gay
Oregon State University
19:20
15m
Talk
Latent Effects for Reusable Language Components
Virtual
Research Papers
Birthe van den Berg
KU Leuven
Casper Bach
Delft University of Technology
Tom Schrijvers
KU Leuven
Nicolas Wu
Imperial College London, UK
19:35
15m
Talk
The Choice Construct in the Soufflé Language
Virtual
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
20m
Live Q&A
Q&A and discussion
Virtual
Research Papers
21:50 - 23:10
Verification / Theory (mirror)
Research Papers
at
Zurich D
Chair(s):
Yue Li
Nanjing University
21:50
15m
Talk
Preprocessing of Alternating Automata for Language Emptiness Testing
Virtual
Research Papers
Pavol Vargovčík
Brno University of Technology, Czech Republic
Lukáš Holík
Brno University of Technology
22:05
15m
Talk
Proving LTL Properties of Bitvector Programs and Decompiled Binaries
Virtual
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
15m
Talk
Solving Not-Substring with Flat Abstraction
Virtual
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
15m
Talk
Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program Termination
Virtual
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
20m
Live Q&A
Q&A and discussion
Virtual
Research Papers
Fri 24 Apr 21:04