HATRA 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
VenueSwissotel Chicago
Room nameZurich D
Program

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 1APLAS Keynote Talks at Zurich D +8h
Chair(s): Hakjoo Oh Korea University
09:00
60m
Keynote
Solidifying and Advancing the Software FoundationsVirtual
APLAS Keynote Talks
Zhendong Su ETH Zurich
10:50 - 12:10
Analysis / Synthesis APLAS 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 NetworksVirtual
APLAS 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 SystemsVirtual
APLAS Research Papers
Nobuhiro Kasai Shibaura Institute of Technology, Isao Sasano Shibaura Institute of Technology
11:20
10m
Talk
PyCT: A Python Concolic TesterVirtual
APLAS 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 SpecificationsVirtual
APLAS 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 ProgramsVirtual
APLAS 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 discussionVirtual
APLAS Research Papers

13:50 - 15:10
Compilation / TransformationAPLAS 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 GoVirtual
APLAS 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 MLVirtual
APLAS 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, AbstractlyVirtual
APLAS 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-calculusVirtual
APLAS 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 discussionVirtual
APLAS Research Papers

17:00 - 18:20
Invited talk 1APLAS Keynote Talks at Zurich D
Chair(s): Xinyu Wang University of Michigan
17:00
60m
Keynote
Solidifying and Advancing the Software FoundationsVirtual
APLAS Keynote Talks
Zhendong Su ETH Zurich
18:50 - 20:10
Analysis / Synthesis (mirror)APLAS Research Papers at Zurich D
Chair(s): Kihong Heo KAIST
18:50
15m
Talk
Scalable and Modular Robustness Analysis of Deep Neural NetworksVirtual
APLAS 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 SystemsVirtual
APLAS Research Papers
Nobuhiro Kasai Shibaura Institute of Technology, Isao Sasano Shibaura Institute of Technology
19:20
10m
Talk
PyCT: A Python Concolic TesterVirtual
APLAS 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 SpecificationsVirtual
APLAS 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 ProgramsVirtual
APLAS 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 discussionVirtual
APLAS Research Papers

21:50 - 23:10
Compilation / Transformation (mirror)APLAS Research Papers at Zurich D
Chair(s): Xin Zhang Peking University
21:50
15m
Talk
A Dictionary-Passing Translation of Featherweight GoVirtual
APLAS 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 MLVirtual
APLAS 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, AbstractlyVirtual
APLAS 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-calculusVirtual
APLAS 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 discussionVirtual
APLAS Research Papers

Mon 18 Oct

Displayed time zone: Central Time (US & Canada) change

09:00 - 10:20
Invited talk 2APLAS Keynote Talks at Zurich D +8h
Chair(s): Atsushi Igarashi Kyoto University, Japan
09:00
60m
Keynote
A Separation Logic for Probabilistic IndependenceVirtual
APLAS Keynote Talks
Justin Hsu University of Wisconsin-Madison, USA
10:50 - 12:10
Language DesignAPLAS Research Papers at Zurich D +8h
Chair(s): Sergio Mover Ecole Polytechnique
10:50
15m
Talk
A Typed Programmatic Interface to Contracts on the BlockchainVirtual
APLAS Research Papers
Thi Thu Ha Doan University of Freiburg, Peter Thiemann University of Freiburg, Germany
11:05
15m
Talk
Adaptable Traces for Program ExplanationsVirtual
APLAS 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 ComponentsVirtual
APLAS 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
15m
Talk
The Choice Construct in the Soufflé LanguageVirtual
APLAS 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 discussionVirtual
APLAS Research Papers

13:50 - 15:10
Verification / TheoryAPLAS Research Papers at Zurich D +8h
Chair(s): Xiaokang Qiu Purdue University, USA
13:50
15m
Talk
Preprocessing of Alternating Automata for Language Emptiness TestingVirtual
APLAS 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 BinariesVirtual
APLAS 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 AbstractionVirtual
APLAS 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 TerminationVirtual
APLAS 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 discussionVirtual
APLAS Research Papers

17:00 - 18:20
Invited talk 2APLAS Keynote Talks at Zurich D
Chair(s): Xujie Si McGill University, Canada
17:00
60m
Keynote
A Separation Logic for Probabilistic IndependenceVirtual
APLAS Keynote Talks
Justin Hsu University of Wisconsin-Madison, USA
18:50 - 20:10
Language Design (mirror)APLAS 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 BlockchainVirtual
APLAS Research Papers
Thi Thu Ha Doan University of Freiburg, Peter Thiemann University of Freiburg, Germany
19:05
15m
Talk
Adaptable Traces for Program ExplanationsVirtual
APLAS 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 ComponentsVirtual
APLAS 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
15m
Talk
The Choice Construct in the Soufflé LanguageVirtual
APLAS 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 discussionVirtual
APLAS Research Papers

21:50 - 23:10
Verification / Theory (mirror)APLAS Research Papers at Zurich D
Chair(s): Yue Li Nanjing University
21:50
15m
Talk
Preprocessing of Alternating Automata for Language Emptiness TestingVirtual
APLAS 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 BinariesVirtual
APLAS 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 AbstractionVirtual
APLAS 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 TerminationVirtual
APLAS 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 discussionVirtual
APLAS Research Papers

Tue 19 Oct

Displayed time zone: Central Time (US & Canada) change

07:40 - 09:00
Session 4CSAS at Zurich D
Chair(s): Jerome Feret INRIA Paris
07:40
15m
Talk
Fast and Efficient Bit-Level Precision TuningVirtual
SAS
Assalé Adjé Université de Perpignan Via Domitia, Dorra Ben Khalifa Université de Perpignan Via Domitia, Matthieu Martel Université de Perpignan Via Domitia
07:55
15m
Talk
Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Caterina Urban École normale supérieure
08:10
15m
Talk
Static analysis of ReLU neural networks with tropical polyhedraVirtual
SAS
Eric Goubault Ecole Polytechnique, Sebastien Palumby Ecole Polytechnique, Sylvie Putot École Polytechnique, Louis Rustenholz École Polytechnique, Sriram Sankaranarayanan University of Colorado, Boulder
08:25
15m
Talk
Toward Neural-Network-Guided Program Synthesis and VerificationVirtual
SAS
Naoki Kobayashi University of Tokyo, Japan, Taro Sekiyama National Institute of Informatics, Issei Sato The University of Tokyo, Hiroshi Unno University of Tsukuba
08:40
20m
Live Q&A
Session 4C Discussion, Questions and AnswersVirtual
SAS

10:50 - 12:10
Session 2CSAS at Zurich D
Chair(s): Cezara Drăgoi Inria / ENS / Informal Systems
10:50
80m
Talk
Pointer Analysis of Bytecode Programs for Effective Formal Verification of Smart ContractsInvited TalkVirtual
SAS
Mooly Sagiv Tel Aviv University
13:50 - 15:10
Session 3CSAS at Zurich D +8h
Chair(s): David Pichardie Facebook Paris
13:50
15m
Talk
Automatic Synthesis of Data-Flow AnalyzersVirtual
SAS
Xuezheng Xu UNSW Sydney, Xudong Wang UNSW Sydney, Jingling Xue UNSW Sydney
14:05
15m
Talk
Disjunctive Interval AnalysisVirtual
SAS
14:20
15m
Talk
Hash Consed Points-To SetsVirtual
SAS
Mohamad Barbar University of Technology Sydney; CSIRO’s Data61, Yulei Sui University of New South Wales, Sydney
14:35
15m
Talk
Selective Context-Sensitivity for k-CFA with CFL-ReachabilityVirtual
SAS
Jingbo Lu UNSW Sydney, Dongjie He UNSW Sydney, Jingling Xue UNSW Sydney
14:50
20m
Live Q&A
Session 3C Discussion, Questions and Answers
SAS

15:40 - 17:00
Session 4CSAS at Zurich D -8h
Chair(s): Suvam Mukherjee Microsoft Research
15:40
15m
Talk
Fast and Efficient Bit-Level Precision TuningVirtual
SAS
Assalé Adjé Université de Perpignan Via Domitia, Dorra Ben Khalifa Université de Perpignan Via Domitia, Matthieu Martel Université de Perpignan Via Domitia
15:55
15m
Talk
Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Caterina Urban École normale supérieure
16:10
15m
Talk
Static analysis of ReLU neural networks with tropical polyhedraVirtual
SAS
Eric Goubault Ecole Polytechnique, Sebastien Palumby Ecole Polytechnique, Sylvie Putot École Polytechnique, Louis Rustenholz École Polytechnique, Sriram Sankaranarayanan University of Colorado, Boulder
16:25
15m
Talk
Toward Neural-Network-Guided Program Synthesis and VerificationVirtual
SAS
Naoki Kobayashi University of Tokyo, Japan, Taro Sekiyama National Institute of Informatics, Issei Sato The University of Tokyo, Hiroshi Unno University of Tsukuba
16:40
20m
Live Q&A
Session 4C Discussion, Questions and AnswersVirtual
SAS

21:50 - 23:10
Session 3CSAS at Zurich D
Chair(s): Kedar Namjoshi Nokia Bell Labs
21:50
15m
Talk
Automatic Synthesis of Data-Flow AnalyzersVirtual
SAS
Xuezheng Xu UNSW Sydney, Xudong Wang UNSW Sydney, Jingling Xue UNSW Sydney
22:05
15m
Talk
Disjunctive Interval AnalysisVirtual
SAS
22:20
15m
Talk
Hash Consed Points-To SetsVirtual
SAS
Mohamad Barbar University of Technology Sydney; CSIRO’s Data61, Yulei Sui University of New South Wales, Sydney
22:35
15m
Talk
Selective Context-Sensitivity for k-CFA with CFL-ReachabilityVirtual
SAS
Jingbo Lu UNSW Sydney, Dongjie He UNSW Sydney, Jingling Xue UNSW Sydney
22:50
20m
Live Q&A
Session 3C Discussion, Questions and Answers
SAS

Wed 20 Oct

Displayed time zone: Central Time (US & Canada) change

07:40 - 09:00
Shared Memory - mirrorSPLASH OOPSLA at Zurich D
Chair(s): Sebastian Burckhardt Microsoft Research
07:40
15m
Talk
The Semantics of Shared Memory in Intel CPU/FPGA SystemsVirtual
SPLASH OOPSLA
Dan Iorga Imperial College London, Alastair F. Donaldson Imperial College London, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
DOI
07:55
15m
Talk
SecRSL: Security Separation Logic for C11 Release-Acquire ConcurrencyVirtual
SPLASH OOPSLA
Pengbo Yan University of Melbourne, Toby Murray University of Melbourne
DOI
08:10
15m
Talk
The Reads-From Equivalence for the TSO and PSO Memory ModelsVirtual
SPLASH OOPSLA
Truc Lam Bui Comenius University Bratislava, Krishnendu Chatterjee IST Austria, Tushar Gautam IIT Bombay, Andreas Pavlogiannis Aarhus University, Viktor Toman IST Austria
DOI
08:25
15m
Talk
Making Weak Memory Models FairDistinguished PaperVirtual
SPLASH OOPSLA
Ori Lahav Tel Aviv University, Egor Namakonov St. Petersburg University; JetBrains Research, Jonas Oberhauser Huawei, Anton Podkopaev HSE University; JetBrains Research, Viktor Vafeiadis MPI-SWS
DOI
08:40
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

09:00 - 09:01
SPLASH StartSPLASH Opening at Zurich D
09:00
1m
Day opening
SPLASH Conference at Chicago Starts NowIn-Person
SPLASH Opening

09:00 - 09:20
Opening SessionSPLASH Opening at Zurich D +8h
09:00
20m
Day opening
Opening SessionIn-Person
SPLASH Opening
Hridesh Rajan Iowa State University
09:20 - 10:20
SPLASH KeynoteSPLASH Keynotes at Zurich D +8h
09:20
60m
Keynote
Exascale and then what?: HPC and AI for Scientific DiscoveryKeynote
SPLASH Keynotes
K: Rick Stevens Argonne National Laboratory
10:20 - 10:50
Posters Virtual SessionSPLASH Posters at Zurich D +8h
10:20
30m
Poster
SkyQuery: An Aerial Drone Video Sensing PlatformVirtualOnward! Papers
SPLASH Posters
Favyen Bastani Massachusetts Institute of Technology, Songtao He Massachusetts Institute of Technology, Ziwen Jiang Massachusetts Institute of Technology, Osbert Bastani University of Pennsylvania, Sam Madden Massachusetts Institute of Technology
10:20
30m
Poster
Dala: A Simple Capability-Based Dynamic Language Design For Data Race-FreedomVirtualOnward! Papers
SPLASH Posters
Kiko Fernandez-Reyes Uppsala University, Isaac Oscar Gariano Victoria University of Wellington, James Noble Victoria University of Wellington, Erin Greenwood-Thessman Victoria University of Wellington, Michael Homer Victoria University of Wellington, Tobias Wrigstad Uppsala University, Sweden
10:20
30m
Poster
Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed SystemsVirtualOOPSLA
SPLASH Posters
Wolf Honore Yale University, Jieung Kim Yale University, Ji-Yong Shin Northeastern University, Zhong Shao Yale University
10:20
30m
Poster
The Semantics of Shared Memory in Intel CPU/FPGA SystemsVirtualOOPSLA
SPLASH Posters
Dan Iorga Imperial College London, Alastair F. Donaldson Imperial College London, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
10:20
30m
Poster
Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional ProgramsIn-Person and VirtualOOPSLA
SPLASH Posters
Yuyan Bao University of Waterloo, Guannan Wei Purdue University, Oliver Bračevac Purdue University, Yuxuan Jiang Purdue University, Qiyang He Purdue University, Tiark Rompf Purdue University
10:20
30m
Poster
Towards Self-Adaptable LanguagesVirtualOnward! Papers
SPLASH Posters
Gwendal Jouneaux University of Rennes; Inria; IRISA, Olivier Barais University of Rennes; Inria; IRISA, Benoit Combemale University of Rennes; Inria; IRISA, Gunter Mussbacher McGill University
10:50 - 12:10
Functional ProgrammingSPLASH OOPSLA at Zurich D +8h
Chair(s): Nada Amin Harvard University
10:50
15m
Talk
Compiling with Continuations, CorrectlyVirtual
SPLASH OOPSLA
Zoe Paraskevopoulou Northeastern University, Anvay Grover University of Wisconsin-Madison
DOI
11:05
15m
Talk
Synbit: Synthesizing Bidirectional Programs using Unidirectional SketchesVirtual
SPLASH OOPSLA
Masaomi Yamaguchi Tohoku University, Kazutaka Matsuda Tohoku University, Cristina David University of Bristol, Meng Wang University of Bristol
DOI
11:20
15m
Talk
Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional ProgramsVirtual
SPLASH OOPSLA
Yuyan Bao University of Waterloo, Guannan Wei Purdue University, Oliver Bračevac Purdue University, Yuxuan Jiang Purdue University, Qiyang He Purdue University, Tiark Rompf Purdue University
DOI
11:35
15m
Talk
Efficient Compilation of Algebraic Effect HandlersVirtual
SPLASH OOPSLA
Georgios Karachalias Tweag, Filip Koprivec University of Ljubljana; Institute of Mathematics, Matija Pretnar University of Ljubljana; Institute of Mathematics, Tom Schrijvers KU Leuven
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

13:50 - 15:10
RustSPLASH OOPSLA at Zurich D +8h
Chair(s): Nadia Polikarpova University of California at San Diego
13:50
15m
Talk
Translating C to Safer RustVirtual
SPLASH OOPSLA
Mehmet Emre University of California at Santa Barbara, Ryan Schroeder University of California at Santa Barbara, Kyle Dewey California State University at Northridge, Ben Hardekopf University of California at Santa Barbara
DOI
14:05
15m
Talk
Modular Specification and Verification of Closures in RustVirtual
SPLASH OOPSLA
Fabian Wolff , Aurel Bílý ETH Zurich, Christoph Matheja ETH Zurich, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia
DOI
14:20
15m
Talk
Safer at Any Speed: Automatic Context-Aware Safety Enhancement for RustVirtual
SPLASH OOPSLA
Natalie Popescu Princeton University, Ziyang Xu Princeton University, Sotiris Apostolakis Google, David I. August Princeton University, Amit Levy Princeton University
DOI
14:35
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

15:40 - 17:00
Shared MemorySPLASH OOPSLA at Zurich D -8h
Chair(s): Doug Lea State University of New York (SUNY) Oswego
15:40
15m
Talk
The Semantics of Shared Memory in Intel CPU/FPGA SystemsVirtual
SPLASH OOPSLA
Dan Iorga Imperial College London, Alastair F. Donaldson Imperial College London, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
DOI
15:55
15m
Talk
SecRSL: Security Separation Logic for C11 Release-Acquire ConcurrencyVirtual
SPLASH OOPSLA
Pengbo Yan University of Melbourne, Toby Murray University of Melbourne
DOI
16:10
15m
Talk
The Reads-From Equivalence for the TSO and PSO Memory ModelsVirtual
SPLASH OOPSLA
Truc Lam Bui Comenius University Bratislava, Krishnendu Chatterjee IST Austria, Tushar Gautam IIT Bombay, Andreas Pavlogiannis Aarhus University, Viktor Toman IST Austria
DOI
16:25
15m
Talk
Making Weak Memory Models FairDistinguished PaperVirtual
SPLASH OOPSLA
Ori Lahav Tel Aviv University, Egor Namakonov St. Petersburg University; JetBrains Research, Jonas Oberhauser Huawei, Anton Podkopaev HSE University; JetBrains Research, Viktor Vafeiadis MPI-SWS
DOI
16:40
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

17:00 - 17:20
Opening SessionSPLASH Opening at Zurich D
17:00
20m
Day opening
Opening SessionIn-Person
SPLASH Opening
Hridesh Rajan Iowa State University
17:20 - 18:20
SPLASH KeynoteSPLASH Keynotes at Zurich D
17:20
60m
Keynote
Exascale and then what?: HPC and AI for Scientific DiscoveryKeynote
SPLASH Keynotes
K: Rick Stevens Argonne National Laboratory
18:20 - 18:50
Posters Virtual SessionSPLASH Posters at Zurich D
18:20
30m
Poster
SkyQuery: An Aerial Drone Video Sensing PlatformVirtualOnward! Papers
SPLASH Posters
Favyen Bastani Massachusetts Institute of Technology, Songtao He Massachusetts Institute of Technology, Ziwen Jiang Massachusetts Institute of Technology, Osbert Bastani University of Pennsylvania, Sam Madden Massachusetts Institute of Technology
18:20
30m
Poster
The Semantics of Shared Memory in Intel CPU/FPGA SystemsVirtualOOPSLA
SPLASH Posters
Dan Iorga Imperial College London, Alastair F. Donaldson Imperial College London, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
18:20
30m
Poster
Dala: A Simple Capability-Based Dynamic Language Design For Data Race-FreedomVirtualOnward! Papers
SPLASH Posters
Kiko Fernandez-Reyes Uppsala University, Isaac Oscar Gariano Victoria University of Wellington, James Noble Victoria University of Wellington, Erin Greenwood-Thessman Victoria University of Wellington, Michael Homer Victoria University of Wellington, Tobias Wrigstad Uppsala University, Sweden
18:20
30m
Poster
Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional ProgramsIn-Person and VirtualOOPSLA
SPLASH Posters
Yuyan Bao University of Waterloo, Guannan Wei Purdue University, Oliver Bračevac Purdue University, Yuxuan Jiang Purdue University, Qiyang He Purdue University, Tiark Rompf Purdue University
18:20
30m
Poster
Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed SystemsVirtualOOPSLA
SPLASH Posters
Wolf Honore Yale University, Jieung Kim Yale University, Ji-Yong Shin Northeastern University, Zhong Shao Yale University
18:20
30m
Poster
Towards Self-Adaptable LanguagesVirtualOnward! Papers
SPLASH Posters
Gwendal Jouneaux University of Rennes; Inria; IRISA, Olivier Barais University of Rennes; Inria; IRISA, Benoit Combemale University of Rennes; Inria; IRISA, Gunter Mussbacher McGill University
18:50 - 20:10
Functional Programming - MirrorSPLASH OOPSLA at Zurich D
Chair(s): Atsushi Igarashi Kyoto University, Japan
18:50
15m
Talk
Compiling with Continuations, CorrectlyVirtual
SPLASH OOPSLA
Zoe Paraskevopoulou Northeastern University, Anvay Grover University of Wisconsin-Madison
DOI
19:05
15m
Talk
Synbit: Synthesizing Bidirectional Programs using Unidirectional SketchesVirtual
SPLASH OOPSLA
Masaomi Yamaguchi Tohoku University, Kazutaka Matsuda Tohoku University, Cristina David University of Bristol, Meng Wang University of Bristol
DOI
19:20
15m
Talk
Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional ProgramsVirtual
SPLASH OOPSLA
Yuyan Bao University of Waterloo, Guannan Wei Purdue University, Oliver Bračevac Purdue University, Yuxuan Jiang Purdue University, Qiyang He Purdue University, Tiark Rompf Purdue University
DOI
19:35
15m
Talk
Efficient Compilation of Algebraic Effect HandlersVirtual
SPLASH OOPSLA
Georgios Karachalias Tweag, Filip Koprivec University of Ljubljana; Institute of Mathematics, Matija Pretnar University of Ljubljana; Institute of Mathematics, Tom Schrijvers KU Leuven
DOI
19:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

21:50 - 23:10
Rust - mirrorSPLASH OOPSLA at Zurich D
Chair(s): Toby Murray University of Melbourne
21:50
15m
Talk
Translating C to Safer RustVirtual
SPLASH OOPSLA
Mehmet Emre University of California at Santa Barbara, Ryan Schroeder University of California at Santa Barbara, Kyle Dewey California State University at Northridge, Ben Hardekopf University of California at Santa Barbara
DOI
22:05
15m
Talk
Modular Specification and Verification of Closures in RustVirtual
SPLASH OOPSLA
Fabian Wolff , Aurel Bílý ETH Zurich, Christoph Matheja ETH Zurich, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia
DOI
22:20
15m
Talk
Safer at Any Speed: Automatic Context-Aware Safety Enhancement for RustVirtual
SPLASH OOPSLA
Natalie Popescu Princeton University, Ziyang Xu Princeton University, Sotiris Apostolakis Google, David I. August Princeton University, Amit Levy Princeton University
DOI
22:35
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

Thu 21 Oct

Displayed time zone: Central Time (US & Canada) change

07:40 - 09:00
Corpus and User Studies - mirrorSPLASH OOPSLA at Zurich D
Chair(s): Julian Dolby IBM Research, USA
07:40
15m
Talk
Well-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM CompilersVirtual
SPLASH OOPSLA
Stefanos Chaliasos Athens University of Economics and Business, Thodoris Sotiropoulos Athens University of Economics and Business, Georgios-Petros Drosos Athens University of Economics and Business, Charalambos Ioannis Mitropoulos Technical University of Crete, Dimitris Mitropoulos University of Athens, Diomidis Spinellis Athens University of Economics and Business; Delft University of Technology
DOI
07:55
15m
Talk
How Statically-Typed Functional Programmers Write CodeVirtual
SPLASH OOPSLA
Justin Lubin University of California at Berkeley, Sarah E. Chasins University of California at Berkeley
DOI
08:10
15m
Talk
What We Eval in the Shadows: A Large-Scale Study of Eval in R ProgramsVirtual
SPLASH OOPSLA
Aviral Goel Northeastern University, Pierre Donat-Bouillud Czech Technical University, Filip Křikava Czech Technical University, Christoph Kirsch University of Salzburg; Czech Technical University, Jan Vitek Northeastern University; Czech Technical University
DOI
08:25
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

09:20 - 10:20
SPLASH KeynoteSPLASH Keynotes at Zurich D +8h
Chair(s): Jonathan Aldrich Carnegie Mellon University
09:20
60m
Talk
Integrated Scientific Modeling and Lab AutomationKeynote
SPLASH Keynotes
K: Luca Cardelli University of Oxford
10:20 - 10:50
Posters Virtual SessionSPLASH Posters at Zurich D +8h
10:20
30m
Poster
Coarsening Optimization for Differentiable ProgrammingVirtualOOPSLA
SPLASH Posters
Xipeng Shen North Carolina State University; Facebook, Guoqiang Zhang North Carolina State University; Facebook, Irene Dea Facebook, Samantha Andow Facebook, Emilio Arroyo-Fang Facebook, Neal Gafter Facebook, Johann George Facebook, Melissa Grueter Facebook, Erik Meijer Facebook, Olin Shivers Northeastern University, USA, Steffi Stumpos Facebook, Alanna Tempest Facebook, Christy Warden Facebook, Shannon Yang Facebook
10:20
30m
Poster
Statically Bounded-Memory Delayed Sampling for Probabilistic StreamsIn-Person and VirtualOOPSLA
SPLASH Posters
Eric Atkinson Massachusetts Institute of Technology, Guillaume Baudart IBM Research, USA, Louis Mandel IBM Research, Charles Yuan Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
10:20
30m
Poster
Compilation of Sparse Array Programming ModelsIn-Person and VirtualOOPSLA
SPLASH Posters
Rawn Henry Massachusetts Institute of Technology, Olivia Hsu Stanford University, Rohan Yadav Stanford University, Stephen Chou Massachusetts Institute of Technology, Kunle Olukotun Stanford University, Saman Amarasinghe Massachusetts Institute of Technology, Fredrik Kjolstad Stanford University
10:20
30m
Poster
Study of the Subtyping Machine of Nominal Subtyping with VarianceVirtualDemoOOPSLA
SPLASH Posters
Ori Roth Technion
10:50 - 12:10
Specification SynthesisSPLASH OOPSLA at Zurich D +8h
Chair(s): Zoe Paraskevopoulou Northeastern University
10:50
15m
Talk
Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence RelationsVirtual
SPLASH OOPSLA
Didier Ishimwe University of Nebraska-Lincoln, KimHao Nguyen University of Nebraska-Lincoln, ThanhVu Nguyen George Mason University
DOI
11:05
15m
Talk
Static Detection of Silent Misconfigurations with Deep Interaction AnalysisIn-Person
SPLASH OOPSLA
Jialu Zhang Yale University, Ruzica Piskac Yale University, Ennan Zhai Alibaba Group, Tianyin Xu University of Illinois at Urbana-Champaign
DOI
11:20
15m
Talk
Data-Driven Abductive Inference of Library SpecificationsIn-Person
SPLASH OOPSLA
Zhe Zhou Purdue University, Robert Dickerson Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
DOI
11:35
15m
Talk
Synthesizing Contracts Correct Modulo a Test GeneratorIn-Person
SPLASH OOPSLA
Angello Astorga University of Illinois at Urbana-Champaign, Shambwaditya Saha Tufts University, Ahmad Dinkins University of Illinois at Urbana-Champaign, Felicia Wang University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Tao Xie Peking University
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

13:50 - 15:10
TypesSPLASH OOPSLA at Zurich D +8h
Chair(s): Christos Dimoulas PLT @ Northwestern University
13:50
15m
Talk
Study of the Subtyping Machine of Nominal Subtyping with VarianceDistinguished PaperVirtual
SPLASH OOPSLA
Ori Roth Technion
DOI Pre-print Media Attached
14:05
15m
Talk
Label Dependent Lambda Calculus and Gradual TypingVirtual
SPLASH OOPSLA
Weili Fu University of Edinburgh, Fabian Krause University of Freiburg, Peter Thiemann University of Freiburg, Germany
DOI
14:20
15m
Talk
Relational Nullable Types with Boolean UnificationVirtual
SPLASH OOPSLA
Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University
DOI
14:35
15m
Talk
Type Stability in Julia: Avoiding Performance Pathologies in JIT CompilationIn-Person
SPLASH OOPSLA
Artem Pelenitsyn Northeastern University, Julia Belyakova Northeastern University, Benjamin Chung Northeastern University, Ross Tate Cornell University, Jan Vitek Northeastern University; Czech Technical University
DOI Pre-print Media Attached
14:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

15:40 - 17:00
Corpus and User StudiesSPLASH OOPSLA at Zurich D -8h
Chair(s): Iulian Neamtiu New Jersey Institute of Technology
15:40
15m
Talk
Well-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM CompilersVirtual
SPLASH OOPSLA
Stefanos Chaliasos Athens University of Economics and Business, Thodoris Sotiropoulos Athens University of Economics and Business, Georgios-Petros Drosos Athens University of Economics and Business, Charalambos Ioannis Mitropoulos Technical University of Crete, Dimitris Mitropoulos University of Athens, Diomidis Spinellis Athens University of Economics and Business; Delft University of Technology
DOI
15:55
15m
Talk
How Statically-Typed Functional Programmers Write CodeVirtual
SPLASH OOPSLA
Justin Lubin University of California at Berkeley, Sarah E. Chasins University of California at Berkeley
DOI
16:10
15m
Talk
What We Eval in the Shadows: A Large-Scale Study of Eval in R ProgramsVirtual
SPLASH OOPSLA
Aviral Goel Northeastern University, Pierre Donat-Bouillud Czech Technical University, Filip Křikava Czech Technical University, Christoph Kirsch University of Salzburg; Czech Technical University, Jan Vitek Northeastern University; Czech Technical University
DOI
16:25
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

17:20 - 18:20
SPLASH KeynoteSPLASH Keynotes at Zurich D
Chair(s): Jonathan Aldrich Carnegie Mellon University
17:20
60m
Talk
Integrated Scientific Modeling and Lab AutomationKeynote
SPLASH Keynotes
K: Luca Cardelli University of Oxford
18:20 - 18:50
Posters Virtual SessionSPLASH Posters at Zurich D
18:20
30m
Poster
Study of the Subtyping Machine of Nominal Subtyping with VarianceVirtualDemoOOPSLA
SPLASH Posters
Ori Roth Technion
18:20
30m
Poster
Statically Bounded-Memory Delayed Sampling for Probabilistic StreamsIn-Person and VirtualOOPSLA
SPLASH Posters
Eric Atkinson Massachusetts Institute of Technology, Guillaume Baudart IBM Research, USA, Louis Mandel IBM Research, Charles Yuan Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
18:20
30m
Poster
Compilation of Sparse Array Programming ModelsIn-Person and VirtualOOPSLA
SPLASH Posters
Rawn Henry Massachusetts Institute of Technology, Olivia Hsu Stanford University, Rohan Yadav Stanford University, Stephen Chou Massachusetts Institute of Technology, Kunle Olukotun Stanford University, Saman Amarasinghe Massachusetts Institute of Technology, Fredrik Kjolstad Stanford University
18:20
30m
Poster
Coarsening Optimization for Differentiable ProgrammingVirtualOOPSLA
SPLASH Posters
Xipeng Shen North Carolina State University; Facebook, Guoqiang Zhang North Carolina State University; Facebook, Irene Dea Facebook, Samantha Andow Facebook, Emilio Arroyo-Fang Facebook, Neal Gafter Facebook, Johann George Facebook, Melissa Grueter Facebook, Erik Meijer Facebook, Olin Shivers Northeastern University, USA, Steffi Stumpos Facebook, Alanna Tempest Facebook, Christy Warden Facebook, Shannon Yang Facebook
18:50 - 20:10
Specification Synthesis - mirrorSPLASH OOPSLA at Zurich D
Chair(s): Toby Murray University of Melbourne
18:50
15m
Talk
Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence RelationsVirtual
SPLASH OOPSLA
Didier Ishimwe University of Nebraska-Lincoln, KimHao Nguyen University of Nebraska-Lincoln, ThanhVu Nguyen George Mason University
DOI
19:05
15m
Talk
Static Detection of Silent Misconfigurations with Deep Interaction AnalysisIn-Person
SPLASH OOPSLA
Jialu Zhang Yale University, Ruzica Piskac Yale University, Ennan Zhai Alibaba Group, Tianyin Xu University of Illinois at Urbana-Champaign
DOI
19:20
15m
Talk
Data-Driven Abductive Inference of Library SpecificationsIn-Person
SPLASH OOPSLA
Zhe Zhou Purdue University, Robert Dickerson Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
DOI
19:35
15m
Talk
Synthesizing Contracts Correct Modulo a Test GeneratorIn-Person
SPLASH OOPSLA
Angello Astorga University of Illinois at Urbana-Champaign, Shambwaditya Saha Tufts University, Ahmad Dinkins University of Illinois at Urbana-Champaign, Felicia Wang University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Tao Xie Peking University
DOI
19:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

21:50 - 23:10
Types - mirrorSPLASH OOPSLA at Zurich D
Chair(s): Wei-Ngan Chin National University of Singapore
21:50
15m
Talk
Study of the Subtyping Machine of Nominal Subtyping with VarianceDistinguished PaperVirtual
SPLASH OOPSLA
Ori Roth Technion
DOI Pre-print Media Attached
22:05
15m
Talk
Label Dependent Lambda Calculus and Gradual TypingVirtual
SPLASH OOPSLA
Weili Fu University of Edinburgh, Fabian Krause University of Freiburg, Peter Thiemann University of Freiburg, Germany
DOI
22:20
15m
Talk
Relational Nullable Types with Boolean UnificationVirtual
SPLASH OOPSLA
Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University
DOI
22:35
15m
Talk
Type Stability in Julia: Avoiding Performance Pathologies in JIT CompilationIn-Person
SPLASH OOPSLA
Artem Pelenitsyn Northeastern University, Julia Belyakova Northeastern University, Benjamin Chung Northeastern University, Ross Tate Cornell University, Jan Vitek Northeastern University; Czech Technical University
DOI Pre-print Media Attached
22:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

Fri 22 Oct

Displayed time zone: Central Time (US & Canada) change

09:00 - 09:05
SPLASH 2022 IntroductionSPLASH Opening at Zurich D +8h
09:00
5m
Other
Introduction to SPLASH 2022
SPLASH Opening
Alex Potanin Victoria University of Wellington
09:05 - 09:20
AwardsSPLASH Awards at Zurich D +8h
Chair(s): Işıl Dillig University of Texas at Austin, Sophia Drossopoulou Facebook and Imperial College London
09:05
15m
Awards
SPLASH Awards
SPLASH Awards

09:20 - 10:20
Onward! Keynote TalkSPLASH Onward! Papers at Zurich D +8h
Chair(s): Wolfgang De Meuter Vrije Universiteit Brussel
09:20
60m
Keynote
Designing Safe Programmed Molecular SystemsVirtualKeynote
SPLASH Onward! Papers
K: Robyn Lutz Iowa State University
10:20 - 10:50
Posters Virtual SessionSPLASH Posters at Zurich D +8h
10:20
30m
Poster
Formal Verification of High-Level SynthesisVirtualDemoOOPSLA
SPLASH Posters
Yann Herklotz Imperial College London, James D. Pollard Imperial College London, Nadesh Ramanathan Imperial College London, John Wickerson Imperial College London
10:20
30m
Poster
Scalability and Precision by Combining Expressive Type Systems and Deductive VerificationVirtualDemoOOPSLA
SPLASH Posters
Florian Lanzinger KIT, Alexander Weigl KIT, Mattias Ulbrich KIT, Werner Dietl University of Waterloo
10:50 - 12:10
Synthesis of models, tools and programsSPLASH OOPSLA at Zurich D +8h
Chair(s): Jonathan Aldrich Carnegie Mellon University
10:50
15m
Talk
Rewrite Rule Inference Using Equality SaturationDistinguished PaperVirtual
SPLASH OOPSLA
Chandrakana Nandi Certora, inc., Max Willsey University of Washington, Amy Zhu University of Washington, Yisu Remy Wang University of Washington, Brett Saiki University of Washington, Adam Anderson University of Washington, Adriana Schulz University of Washington, Dan Grossman University of Washington, Zachary Tatlock University of Washington
DOI
11:05
15m
Talk
Semantic Programming by Example with Pre-trained ModelsVirtual
SPLASH OOPSLA
Gust Verbruggen KU Leuven, Vu Le Microsoft, Sumit Gulwani Microsoft
DOI
11:20
15m
Talk
One Down, 699 to Go: or, Synthesising Compositional DesugaringsVirtual
SPLASH OOPSLA
Sándor Bartha University of Edinburgh, James Cheney University of Edinburgh; Alan Turing Institute, Vaishak Belle University of Edinburgh; Alan Turing Institute
DOI
11:35
15m
Talk
Multi-modal Program Inference: A Marriage of Pre-trained Language Models and Component-Based SynthesisIn-Person
SPLASH OOPSLA
Kia Rahmani Purdue University, Mohammad Raza Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Daniel Morris Microsoft, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Ashish Tiwari Microsoft
DOI Pre-print
11:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

13:50 - 15:10
Types & VerificationSPLASH OOPSLA at Zurich D +8h
Chair(s): Leonidas Lampropoulos University of Maryland, College Park
13:50
15m
Talk
Scalability and Precision by Combining Expressive Type Systems and Deductive VerificationVirtual
SPLASH OOPSLA
Florian Lanzinger KIT, Alexander Weigl KIT, Mattias Ulbrich KIT, Werner Dietl University of Waterloo
DOI
14:05
15m
Talk
A Type System for Extracting Functional Specifications from Memory-Safe Imperative ProgramsVirtual
SPLASH OOPSLA
Paul He University of Pennsylvania, Edwin Westbrook Galois, Brent Carmer Galois, Chris Phifer Galois, Valentin Robert Galois, Karl Smeltzer Galois, Andrei Ştefănescu Galois, Aaron Tomb Galois, Adam Wick Galois, Matthew Yacavone Galois, Steve Zdancewic University of Pennsylvania
DOI
14:20
15m
Talk
Transitioning from Structural to Nominal Code with Efficient Gradual TypingIn-Person
SPLASH OOPSLA
Fabian Muehlboeck IST Austria, Ross Tate Cornell University
DOI
14:35
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

15:10 - 17:00
Closing SessionSPLASH Closing at Zurich D
15:10
1h50m
Day closing
Ice Cream Social
SPLASH Closing
Hridesh Rajan Iowa State University
17:00 - 17:05
SPLASH 2022 IntroductionSPLASH Opening at Zurich D
17:00
5m
Other
Introduction to SPLASH 2022
SPLASH Opening
Alex Potanin Victoria University of Wellington
17:05 - 17:20
17:05
15m
Awards
SPLASH Awards
SPLASH Awards

17:20 - 18:20
Onward! Keynote TalkSPLASH Onward! Papers at Zurich D
Chair(s): Elisa Baniassad University of British Columbia
17:20
60m
Keynote
Designing Safe Programmed Molecular SystemsVirtualKeynote
SPLASH Onward! Papers
K: Robyn Lutz Iowa State University
18:20 - 18:50
Posters Virtual SessionSPLASH Posters at Zurich D
18:20
30m
Poster
Scalability and Precision by Combining Expressive Type Systems and Deductive VerificationVirtualDemoOOPSLA
SPLASH Posters
Florian Lanzinger KIT, Alexander Weigl KIT, Mattias Ulbrich KIT, Werner Dietl University of Waterloo
18:20
30m
Poster
Formal Verification of High-Level SynthesisVirtualDemoOOPSLA
SPLASH Posters
Yann Herklotz Imperial College London, James D. Pollard Imperial College London, Nadesh Ramanathan Imperial College London, John Wickerson Imperial College London
18:50 - 20:10
Synthesis of models, tools and programs -- mirrorSPLASH OOPSLA at Zurich D
Chair(s): Alex Potanin Victoria University of Wellington
18:50
15m
Talk
Rewrite Rule Inference Using Equality SaturationDistinguished PaperVirtual
SPLASH OOPSLA
Chandrakana Nandi Certora, inc., Max Willsey University of Washington, Amy Zhu University of Washington, Yisu Remy Wang University of Washington, Brett Saiki University of Washington, Adam Anderson University of Washington, Adriana Schulz University of Washington, Dan Grossman University of Washington, Zachary Tatlock University of Washington
DOI
19:05
15m
Talk
Semantic Programming by Example with Pre-trained ModelsVirtual
SPLASH OOPSLA
Gust Verbruggen KU Leuven, Vu Le Microsoft, Sumit Gulwani Microsoft
DOI
19:20
15m
Talk
One Down, 699 to Go: or, Synthesising Compositional DesugaringsVirtual
SPLASH OOPSLA
Sándor Bartha University of Edinburgh, James Cheney University of Edinburgh; Alan Turing Institute, Vaishak Belle University of Edinburgh; Alan Turing Institute
DOI
19:35
15m
Talk
Multi-modal Program Inference: A Marriage of Pre-trained Language Models and Component-Based SynthesisIn-Person
SPLASH OOPSLA
Kia Rahmani Purdue University, Mohammad Raza Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Daniel Morris Microsoft, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Ashish Tiwari Microsoft
DOI Pre-print
19:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

21:50 - 23:10
Types & Verification -- mirrorSPLASH OOPSLA at Zurich D
Chair(s): Atsushi Igarashi Kyoto University, Japan
21:50
15m
Talk
Scalability and Precision by Combining Expressive Type Systems and Deductive VerificationVirtual
SPLASH OOPSLA
Florian Lanzinger KIT, Alexander Weigl KIT, Mattias Ulbrich KIT, Werner Dietl University of Waterloo
DOI
22:05
15m
Talk
A Type System for Extracting Functional Specifications from Memory-Safe Imperative ProgramsVirtual
SPLASH OOPSLA
Paul He University of Pennsylvania, Edwin Westbrook Galois, Brent Carmer Galois, Chris Phifer Galois, Valentin Robert Galois, Karl Smeltzer Galois, Andrei Ştefănescu Galois, Aaron Tomb Galois, Adam Wick Galois, Matthew Yacavone Galois, Steve Zdancewic University of Pennsylvania
DOI
22:20
15m
Talk
Transitioning from Structural to Nominal Code with Efficient Gradual TypingIn-Person
SPLASH OOPSLA
Fabian Muehlboeck IST Austria, Ross Tate Cornell University
DOI
22:35
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

Tue 19 Oct

Displayed time zone: Central Time (US & Canada) change

Room7:00308:00309:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:003020:003021:003022:003023:0030
Zurich D

Sun 17 Oct

Displayed time zone: Central Time (US & Canada) change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:0015304522:0015304523:00153045
Zurich D

Mon 18 Oct

Displayed time zone: Central Time (US & Canada) change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:0015304522:0015304523:00153045
Zurich D

Tue 19 Oct

Displayed time zone: Central Time (US & Canada) change

Room7:001530458:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:0015304522:0015304523:00153045
Zurich D

Wed 20 Oct

Displayed time zone: Central Time (US & Canada) change

Room7:001530458:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:0015304522:0015304523:00153045
Zurich D

Thu 21 Oct

Displayed time zone: Central Time (US & Canada) change

Room7:001530458:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:0015304522:0015304523:00153045
Zurich D

Fri 22 Oct

Displayed time zone: Central Time (US & Canada) change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:0015304522:0015304523:00153045
Zurich D