SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
VenueSwissotel Chicago
Room nameZurich B
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
Session 1ASAS at Zurich B +8h
Chair(s): Cezara Drăgoi Inria / ENS / Informal Systems
09:00
15m
Talk
Accelerating Program Analyses in Datalog by Merging Library FactsVirtual
SAS
Yifan Chen Peking University, Chenyang Yang , Xin Zhang Peking University, Yingfei Xiong Peking University, Hao Tang Peking University, Xiaoyin Wang University of Texas at San Antonio, Lu Zhang Peking University
09:15
15m
Talk
Exploiting Verified Neural Networks via Floating Point Numerical ErrorVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard
Pre-print
09:30
15m
Talk
Verifying Low-dimensional Input Neural Networks via Input QuantizationVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology
Pre-print
09:45
15m
Talk
A Multi-Language Static Analysis of Python Programs with Native C ExtensionsVirtual
SAS
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Pre-print Media Attached
10:00
20m
Live Q&A
Session 1A Discussion, Questions and Answers Virtual
SAS

13:50 - 15:10
Session 3ASAS at Zurich B +8h
Chair(s): Mihaela Sighireanu IRIF, Université Paris Diderot, France
13:50
15m
Talk
Static Analysis of Endian Portability by Abstract InterpretationVirtual
SAS
David Delmas Airbus & Sorbonne Université, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
14:05
15m
Talk
Verified Functional Programming of an Abstract InterpreterVirtual
SAS
Lucas Franceschino INRIA, David Pichardie Facebook Paris, Jean-Pierre Talpin INRIA, France
14:30
15m
Talk
Data Abstraction: A General Framework to Handle Program Verification of Data StructuresVirtual
SAS
Julien Braine , Laure Gonnord University of Lyon & LIP, France, David Monniaux CNRS/VERIMAG
14:45
25m
Live Q&A
Session 3A Discussion, Questions and AnswersVirtual
SAS

17:00 - 18:20
Session 1ASAS at Zurich B
Chair(s): Kedar Namjoshi Nokia Bell Labs
17:00
15m
Talk
Accelerating Program Analyses in Datalog by Merging Library FactsVirtual
SAS
Yifan Chen Peking University, Chenyang Yang , Xin Zhang Peking University, Yingfei Xiong Peking University, Hao Tang Peking University, Xiaoyin Wang University of Texas at San Antonio, Lu Zhang Peking University
17:15
15m
Talk
Exploiting Verified Neural Networks via Floating Point Numerical ErrorVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard
Pre-print
17:30
15m
Talk
Verifying Low-dimensional Input Neural Networks via Input QuantizationVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology
Pre-print
17:45
15m
Talk
A Multi-Language Static Analysis of Python Programs with Native C ExtensionsVirtual
SAS
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Pre-print Media Attached
18:00
20m
Live Q&A
Session 1A Discussion, Questions and Answers Virtual
SAS

Mon 18 Oct

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

07:40 - 09:00
Session 4BSAS at Zurich B
Chair(s): Antoine Miné Sorbonne Université
07:40
15m
Talk
Automated Verification of the Parallel Bellman--Ford AlgorithmVirtual
SAS
Mohsen Safari University of Twente, The Netherlands, Wytse Oortwijn ETH Zurich, Switzerland, Marieke Huisman University of Twente
07:55
15m
Talk
Backward Symbolic Execution with Loop FoldingVirtual
SAS
Marek Chalupa Masaryk University, Jan Strejcek Masaryk University
08:10
15m
Talk
Improving Thread-Modular Abstract InterpretationVirtual
SAS
Michael Schwarz Technische Universität München, Simmo Saan University of Tartu, Estonia, Helmut Seidl Technische Universität München, Kalmer Apinis University of Tartu, Estonia, Julian Erhard , Vesal Vojdani University of Tartu
Pre-print Media Attached
08:25
15m
Talk
Symbolic Automatic Relations and Their Applications to SMT and CHC SolvingVirtual
SAS
Takumi Shimoda The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan
08:40
20m
Live Q&A
Session 4B Discussion, Questions and Answers
SAS

10:50 - 12:10
Session 2BSAS at Zurich B +8h
Chair(s): Cezara Drăgoi Inria / ENS / Informal Systems
10:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication AbstractionVirtual
SAS
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Arie Gurfinkel University of Waterloo, Jorge A. Navas SRI International, Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys
Pre-print
11:05
15m
Talk
Selectively-Amortized Resource BoundingVirtual
SAS
Tianhan Lu University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Ashutosh Trivedi
Pre-print
11:20
15m
Talk
Thread-modular Analysis of Release-Acquire ConcurrencyVirtual
SAS
Divyanjali Sharma IIT Delhi, India, Subodh Sharma IIT Delhi
11:35
35m
Live Q&A
Session 2B Discussion, Questions and Answers
SAS

13:50 - 15:10
Session 3BSAS at Zurich B
Chair(s): Kedar Namjoshi Nokia Bell Labs
13:50
80m
Keynote
Interactive Code AnalysisInvited TalkVirtual
SAS
I: Gerard Holzmann NASA/Caltech Jet Propulsion Laboratory
15:40 - 17:00
Session 4BSAS at Zurich B -8h
Chair(s): Kedar Namjoshi Nokia Bell Labs
15:40
15m
Talk
Automated Verification of the Parallel Bellman--Ford AlgorithmVirtual
SAS
Mohsen Safari University of Twente, The Netherlands, Wytse Oortwijn ETH Zurich, Switzerland, Marieke Huisman University of Twente
15:55
15m
Talk
Backward Symbolic Execution with Loop FoldingVirtual
SAS
Marek Chalupa Masaryk University, Jan Strejcek Masaryk University
16:10
15m
Talk
Improving Thread-Modular Abstract InterpretationVirtual
SAS
Michael Schwarz Technische Universität München, Simmo Saan University of Tartu, Estonia, Helmut Seidl Technische Universität München, Kalmer Apinis University of Tartu, Estonia, Julian Erhard , Vesal Vojdani University of Tartu
Pre-print Media Attached
16:25
15m
Talk
Symbolic Automatic Relations and Their Applications to SMT and CHC SolvingVirtual
SAS
Takumi Shimoda The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan
16:40
20m
Live Q&A
Session 4B Discussion, Questions and Answers
SAS

18:50 - 20:10
Session 2BSAS at Zurich B
Chair(s): Suvam Mukherjee Microsoft Research
18:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication AbstractionVirtual
SAS
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Arie Gurfinkel University of Waterloo, Jorge A. Navas SRI International, Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys
Pre-print
19:05
15m
Talk
Selectively-Amortized Resource BoundingVirtual
SAS
Tianhan Lu University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Ashutosh Trivedi
Pre-print
19:20
15m
Talk
Thread-modular Analysis of Release-Acquire ConcurrencyVirtual
SAS
Divyanjali Sharma IIT Delhi, India, Subodh Sharma IIT Delhi
19:35
35m
Live Q&A
Session 2B Discussion, Questions and Answers
SAS

Tue 19 Oct

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

07:30 - 09:00
07:30
90m
Talk
Hedy: Creating a gradual programming languageVirtual
SPLASH REBASE
Felienne Hermans Leiden University, Federico Tomassetti Independent
09:00 - 10:30
09:00
90m
Talk
The F# view on the Static / Dynamic divideVirtual
SPLASH REBASE
Don Syme Microsoft, Nicholas Matsakis Amazon, USA
13:50 - 15:20
InterfacesSPLASH REBASE at Zurich B
13:50
90m
Talk
A Brief History of the API, RevisitedVirtual
SPLASH REBASE
Josh Bloch Carnegie Mellon University, Doug Lea State University of New York (SUNY) Oswego
15:40 - 17:10
15:40
90m
Talk
Fragmentation of Machine ArchitectureVirtual
SPLASH REBASE
Sean Parent Adobe, Mario Wolczko Oracle Labs

Wed 20 Oct

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

07:40 - 09:00
Distributed Programming - mirrorSPLASH OOPSLA at Zurich B
Chair(s): Shigeru Chiba The University of Tokyo
07:40
15m
Talk
A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed ProgrammingVirtual
SPLASH OOPSLA
Malte Viering TU Darmstadt, Raymond Hu Queen Mary University of London, Patrick Eugster USI Lugano; Purdue University, Lukasz Ziarek University at Buffalo
DOI
07:55
15m
Talk
Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed SystemsIn-Person
SPLASH OOPSLA
Wolf Honore Yale University, Jieung Kim Yale University, Ji-Yong Shin Northeastern University, Zhong Shao Yale University
DOI
08:10
15m
Talk
Automatic Migration from Synchronous to Asynchronous JavaScript APIsIn-Person
SPLASH OOPSLA
Satyajit Gokhale Northeastern University, Alexi Turcotte Northeastern University, Frank Tip Northeastern University
DOI
08:25
15m
Talk
QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based SystemsIn-Person
SPLASH OOPSLA
Nouraldin Jaber Purdue University, Christopher Wagner Purdue University, Swen Jacobs CISPA, Milind Kulkarni Purdue University, Roopsha Samanta Purdue University
DOI
08:40
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

10:50 - 12:10
TestingSPLASH OOPSLA at Zurich B +8h
Chair(s): Iulian Neamtiu New Jersey Institute of Technology
10:50
15m
Talk
Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic BugsVirtual
SPLASH OOPSLA
Ting Su East China Normal University, Yichen Yan East China Normal University, Jue Wang Nanjing University, Jingling Sun East China Normal University, Yiheng Xiong East China Normal University, Geguang Pu East China Normal University, Ke Wang Visa Research, Zhendong Su ETH Zurich
DOI
11:05
15m
Talk
Permchecker: A Toolchain for Debugging Memory Managers with TypestateVirtual
SPLASH OOPSLA
Karl Cronburg Tufts University, Sam Guyer Tufts University
DOI Pre-print
11:20
15m
Talk
Generative Type-Aware Mutation for Testing SMT SolversVirtual
SPLASH OOPSLA
Jiwon Park École Polytechnique, Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
DOI
11:35
15m
Talk
Programming and Execution Models for Parallel Bounded Exhaustive TestingIn-Person
SPLASH OOPSLA
Nader Al Awar University of Texas at Austin, Kush Jain University of Texas at Austin, Chris Rossbach University of Texas at Austin; Katana Graph, Milos Gligoric University of Texas at Austin
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

12:10 - 13:50
Session 1SPLASH Faculty Mentorship Roundtable at Zurich B
Chair(s): Danny Dig University of Colorado Boulder, USA
12:10
1h40m
Meeting
Faculty Mentoring RoundtableIn-Person
SPLASH Faculty Mentorship Roundtable

13:50 - 15:10
SecuritySPLASH OOPSLA at Zurich B +8h
Chair(s): Yannis Smaragdakis University of Athens
13:50
15m
Talk
SpecSafe: Detecting Cache Side Channels in a Speculative WorldVirtual
SPLASH OOPSLA
Robert Brotzman-Smith Pennsylvania State University, Danfeng Zhang Pennsylvania State University, Mahmut Taylan Kandemir Pennsylvania State University, Gang (Gary) Tan Pennsylvania State University
DOI
14:05
15m
Talk
Interpretable Noninterference Measurement and Its Application to Processor DesignsVirtual
SPLASH OOPSLA
Ziqiao Zhou Microsoft Research, Michael K. Reiter Duke University
DOI
14:20
15m
Talk
Reconciling Optimization with Secure CompilationVirtual
SPLASH OOPSLA
Son Tuan Vu Sorbonne University; CNRS; LIP6, Albert Cohen Google, Arnaud de Grandmaison ARM, Christophe Guillon STMicroelectronics, Karine Heydemann Sorbonne University; CNRS; LIP6
DOI
14:35
15m
Talk
Not So Fast: Understanding and Mitigating Negative Impacts of Compiler Optimizations on Code Reuse Gadget SetsIn-Person
SPLASH OOPSLA
Michael D. Brown Georgia Institute of Technology, Matthew Pruett Georgia Institute of Technology, Robert Bigelow Georgia Institute of Technology, Girish Mururu Georgia Institute of Technology, Santosh Pande Georgia Institute of Technology
DOI
14:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

15:40 - 17:00
Distributed ProgrammingSPLASH OOPSLA at Zurich B -8h
Chair(s): Mohsen Lesani University of California at Riverside
15:40
15m
Talk
A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed ProgrammingVirtual
SPLASH OOPSLA
Malte Viering TU Darmstadt, Raymond Hu Queen Mary University of London, Patrick Eugster USI Lugano; Purdue University, Lukasz Ziarek University at Buffalo
DOI
15:55
15m
Talk
Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed SystemsIn-Person
SPLASH OOPSLA
Wolf Honore Yale University, Jieung Kim Yale University, Ji-Yong Shin Northeastern University, Zhong Shao Yale University
DOI
16:10
15m
Talk
Automatic Migration from Synchronous to Asynchronous JavaScript APIsIn-Person
SPLASH OOPSLA
Satyajit Gokhale Northeastern University, Alexi Turcotte Northeastern University, Frank Tip Northeastern University
DOI
16:25
15m
Talk
QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based SystemsIn-Person
SPLASH OOPSLA
Nouraldin Jaber Purdue University, Christopher Wagner Purdue University, Swen Jacobs CISPA, Milind Kulkarni Purdue University, Roopsha Samanta Purdue University
DOI
16:40
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

17:00 - 18:50
17:00
1h50m
Other
ReceptionIn-Person
SPLASH Opening

18:50 - 20:10
Testing - MirrorSPLASH OOPSLA at Zurich B
Chair(s): Steve Blackburn Australian National University
18:50
15m
Talk
Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic BugsVirtual
SPLASH OOPSLA
Ting Su East China Normal University, Yichen Yan East China Normal University, Jue Wang Nanjing University, Jingling Sun East China Normal University, Yiheng Xiong East China Normal University, Geguang Pu East China Normal University, Ke Wang Visa Research, Zhendong Su ETH Zurich
DOI
19:05
15m
Talk
Permchecker: A Toolchain for Debugging Memory Managers with TypestateVirtual
SPLASH OOPSLA
Karl Cronburg Tufts University, Sam Guyer Tufts University
DOI Pre-print
19:20
15m
Talk
Generative Type-Aware Mutation for Testing SMT SolversVirtual
SPLASH OOPSLA
Jiwon Park École Polytechnique, Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
DOI
19:35
15m
Talk
Programming and Execution Models for Parallel Bounded Exhaustive TestingIn-Person
SPLASH OOPSLA
Nader Al Awar University of Texas at Austin, Kush Jain University of Texas at Austin, Chris Rossbach University of Texas at Austin; Katana Graph, Milos Gligoric University of Texas at Austin
DOI
19:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

21:50 - 23:10
Security - mirrorSPLASH OOPSLA at Zurich B
Chair(s): Chandrakana Nandi Certora, inc.
21:50
15m
Talk
SpecSafe: Detecting Cache Side Channels in a Speculative WorldVirtual
SPLASH OOPSLA
Robert Brotzman-Smith Pennsylvania State University, Danfeng Zhang Pennsylvania State University, Mahmut Taylan Kandemir Pennsylvania State University, Gang (Gary) Tan Pennsylvania State University
DOI
22:05
15m
Talk
Interpretable Noninterference Measurement and Its Application to Processor DesignsVirtual
SPLASH OOPSLA
Ziqiao Zhou Microsoft Research, Michael K. Reiter Duke University
DOI
22:20
15m
Talk
Reconciling Optimization with Secure CompilationVirtual
SPLASH OOPSLA
Son Tuan Vu Sorbonne University; CNRS; LIP6, Albert Cohen Google, Arnaud de Grandmaison ARM, Christophe Guillon STMicroelectronics, Karine Heydemann Sorbonne University; CNRS; LIP6
DOI
22:35
15m
Talk
Not So Fast: Understanding and Mitigating Negative Impacts of Compiler Optimizations on Code Reuse Gadget SetsIn-Person
SPLASH OOPSLA
Michael D. Brown Georgia Institute of Technology, Matthew Pruett Georgia Institute of Technology, Robert Bigelow Georgia Institute of Technology, Girish Mururu Georgia Institute of Technology, Santosh Pande Georgia Institute of Technology
DOI
22:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

Thu 21 Oct

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

07:40 - 09:00
Smart Contracts and Distributed Programming - mirrorSPLASH OOPSLA at Zurich B
Chair(s): Patrick Eugster USI Lugano; Purdue University
07:40
15m
Talk
Rich Specifications for Ethereum Smart Contract VerificationVirtual
SPLASH OOPSLA
Christian Bräm ETH Zurich, Marco Eilers ETH Zurich, Peter Müller ETH Zurich, Robin Sierra ETH Zurich, Alexander J. Summers University of British Columbia
DOI
07:55
15m
Talk
Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart ContractsVirtual
SPLASH OOPSLA
Yannis Smaragdakis University of Athens, Neville Grech University of Malta, Sifis Lagouvardos University of Athens, Konstantinos Triantafyllou University of Athens, Ilias Tsatiris University of Athens
DOI
08:10
15m
Talk
ECROs: Building Global Scale Systems from Sequential CodeVirtual
SPLASH OOPSLA
Kevin De Porre Vrije Universiteit Brussel, Carla Ferreira NOVA School of Science and Technology, Nuno Preguica NOVA School of Science and Technology, Elisa Gonzalez Boix Vrije Universiteit Brussel
DOI
08:25
15m
Talk
Durable Functions: Semantics for Stateful ServerlessIn-Person
SPLASH OOPSLA
Sebastian Burckhardt Microsoft Research, Chris Gillum Microsoft Azure, David Justo Microsoft Azure, Konstantinos Kallas University of Pennsylvania, Connor McMahon Microsoft Azure, Christopher S. Meiklejohn Carnegie Mellon University
DOI
08:40
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

10:50 - 12:10
Dynamic LanguagesSPLASH OOPSLA at Zurich B +8h
Chair(s): Julia Belyakova Northeastern University
10:50
15m
Talk
Gradually Structured DataVirtual
SPLASH OOPSLA
Stefan Malewski University of Chile, Michael Greenberg Stevens Institute of Technology, Éric Tanter University of Chile
DOI Pre-print
11:05
15m
Talk
Solver-Based Gradual Type MigrationVirtual
SPLASH OOPSLA
Luna Phipps-Costin University of Massachusetts at Amherst, Carolyn Jane Anderson Wellesley College, Michael Greenberg Stevens Institute of Technology, Arjun Guha Northeastern University
DOI Pre-print
11:20
15m
Talk
SimTyper: Sound Type Inference for Ruby using Type Equality PredictionVirtual
SPLASH OOPSLA
Milod Kazerounian University of Maryland at College Park, Jeffrey S. Foster Tufts University, Bonan Min Raytheon BBN Technologies
DOI
11:35
15m
Talk
Promises Are Made to Be Broken: Migrating R to Strict SemanticsIn-Person
SPLASH OOPSLA
Aviral Goel Northeastern University, Jan Ječmen Czech Technical University, Sebastián Krynski Czech Technical University, Olivier Flückiger Northeastern University, Jan Vitek Northeastern University; Czech Technical University
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

12:10 - 13:50
Session 2SPLASH Faculty Mentorship Roundtable at Zurich B
Chair(s): Danny Dig University of Colorado Boulder, USA
12:10
1h40m
Meeting
Faculty Mentoring RoundtableIn-Person
SPLASH Faculty Mentorship Roundtable

13:50 - 15:10
Program SynthesisSPLASH OOPSLA at Zurich B +8h
Chair(s): Kedar Namjoshi Nokia Bell Labs
13:50
15m
Talk
Generalizable Synthesis through UnificationVirtual
SPLASH OOPSLA
Ruyi Ji Peking University, Jingtao Xia Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
DOI
14:05
15m
Talk
Gauss: Program Synthesis by Reasoning over GraphsVirtual
SPLASH OOPSLA
Rohan Bavishi University of California at Berkeley, Caroline Lemieux Microsoft Research, Koushik Sen University of California at Berkeley, Ion Stoica University of California at Berkeley
DOI
14:20
15m
Talk
APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in LibrariesVirtual
SPLASH OOPSLA
Xiang Gao National University of Singapore, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Ridwan Salihin Shariffdeen National University of Singapore, Sumit Gulwani Microsoft, Abhik Roychoudhury National University of Singapore
DOI
14:35
15m
Talk
LooPy: Interactive Program Synthesis with Control StructuresVirtual
SPLASH OOPSLA
Kasra Ferdowsi University of California at San Diego, Shraddha Barke University of California at San Diego, Hila Peleg Technion, Sorin Lerner University of California at San Diego, Nadia Polikarpova University of California at San Diego
DOI
14:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

15:40 - 17:00
Smart Contracts and Distributed ProgrammingSPLASH OOPSLA at Zurich B -8h
Chair(s): Mohsen Lesani University of California at Riverside
15:40
15m
Talk
Rich Specifications for Ethereum Smart Contract VerificationVirtual
SPLASH OOPSLA
Christian Bräm ETH Zurich, Marco Eilers ETH Zurich, Peter Müller ETH Zurich, Robin Sierra ETH Zurich, Alexander J. Summers University of British Columbia
DOI
15:55
15m
Talk
Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart ContractsVirtual
SPLASH OOPSLA
Yannis Smaragdakis University of Athens, Neville Grech University of Malta, Sifis Lagouvardos University of Athens, Konstantinos Triantafyllou University of Athens, Ilias Tsatiris University of Athens
DOI
16:10
15m
Talk
ECROs: Building Global Scale Systems from Sequential CodeVirtual
SPLASH OOPSLA
Kevin De Porre Vrije Universiteit Brussel, Carla Ferreira NOVA School of Science and Technology, Nuno Preguica NOVA School of Science and Technology, Elisa Gonzalez Boix Vrije Universiteit Brussel
DOI
16:25
15m
Talk
Durable Functions: Semantics for Stateful ServerlessIn-Person
SPLASH OOPSLA
Sebastian Burckhardt Microsoft Research, Chris Gillum Microsoft Azure, David Justo Microsoft Azure, Konstantinos Kallas University of Pennsylvania, Connor McMahon Microsoft Azure, Christopher S. Meiklejohn Carnegie Mellon University
DOI
16:40
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

17:00 - 18:50
17:00
1h50m
Other
ReceptionIn-Person
SPLASH Opening

18:50 - 20:10
Dynamic Languages - mirrorSPLASH OOPSLA at Zurich B
Chair(s): Julia Belyakova Northeastern University
18:50
15m
Talk
Gradually Structured DataVirtual
SPLASH OOPSLA
Stefan Malewski University of Chile, Michael Greenberg Stevens Institute of Technology, Éric Tanter University of Chile
DOI Pre-print
19:05
15m
Talk
Solver-Based Gradual Type MigrationVirtual
SPLASH OOPSLA
Luna Phipps-Costin University of Massachusetts at Amherst, Carolyn Jane Anderson Wellesley College, Michael Greenberg Stevens Institute of Technology, Arjun Guha Northeastern University
DOI Pre-print
19:20
15m
Talk
SimTyper: Sound Type Inference for Ruby using Type Equality PredictionVirtual
SPLASH OOPSLA
Milod Kazerounian University of Maryland at College Park, Jeffrey S. Foster Tufts University, Bonan Min Raytheon BBN Technologies
DOI
19:35
15m
Talk
Promises Are Made to Be Broken: Migrating R to Strict SemanticsIn-Person
SPLASH OOPSLA
Aviral Goel Northeastern University, Jan Ječmen Czech Technical University, Sebastián Krynski Czech Technical University, Olivier Flückiger Northeastern University, Jan Vitek Northeastern University; Czech Technical University
DOI
19:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

21:50 - 23:10
Program Synthesis - mirrorSPLASH OOPSLA at Zurich B
Chair(s): Hakjoo Oh Korea University
21:50
15m
Talk
Generalizable Synthesis through UnificationVirtual
SPLASH OOPSLA
Ruyi Ji Peking University, Jingtao Xia Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
DOI
22:05
15m
Talk
Gauss: Program Synthesis by Reasoning over GraphsVirtual
SPLASH OOPSLA
Rohan Bavishi University of California at Berkeley, Caroline Lemieux Microsoft Research, Koushik Sen University of California at Berkeley, Ion Stoica University of California at Berkeley
DOI
22:20
15m
Talk
APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in LibrariesVirtual
SPLASH OOPSLA
Xiang Gao National University of Singapore, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Ridwan Salihin Shariffdeen National University of Singapore, Sumit Gulwani Microsoft, Abhik Roychoudhury National University of Singapore
DOI
22:35
15m
Talk
LooPy: Interactive Program Synthesis with Control StructuresVirtual
SPLASH OOPSLA
Kasra Ferdowsi University of California at San Diego, Shraddha Barke University of California at San Diego, Hila Peleg Technion, Sorin Lerner University of California at San Diego, Nadia Polikarpova University of California at San Diego
DOI
22:50
20m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

Fri 22 Oct

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

10:50 - 12:10
OptimizationSPLASH OOPSLA at Zurich B +8h
Chair(s): Fredrik Kjolstad Stanford University
10:50
15m
Talk
Copy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level Languages and BytecodeDistinguished PaperVirtual
SPLASH OOPSLA
Haoran Xu Stanford University, Fredrik Kjolstad Stanford University
DOI Pre-print
11:05
15m
Talk
VESPA: Static Profiling for Binary OptimizationVirtual
SPLASH OOPSLA
Angelica Moreira Federal University of Minas Gerais, Guilherme Ottoni Facebook, Fernando Magno Quintão Pereira Federal University of Minas Gerais
DOI
11:20
15m
Talk
A Derivative-Based Parser Generator for Visibly Pushdown GrammarsIn-Person
SPLASH OOPSLA
Xiaodong Jia Pennsylvania State University, Ashish Kumar Pennsylvania State University, Gang (Gary) Tan Pennsylvania State University
DOI
11:35
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

13:50 - 15:10
Test and VerificationSPLASH OOPSLA at Zurich B +8h
Chair(s): Mike Dodds Galois, Inc.
13:50
15m
Talk
MonkeyDB: Effectively Testing Correctness under Weak Isolation LevelsDistinguished PaperVirtual
SPLASH OOPSLA
Ranadeep Biswas Informal Systems, Diptanshu Kakwani Microsoft, India, Jyothi Vedurada IIT Hyderabad, Constantin Enea University of Paris / IRIF / CNRS, Akash Lal Microsoft Research
DOI
14:05
15m
Talk
Formal Verification of High-Level SynthesisVirtual
SPLASH OOPSLA
Yann Herklotz Imperial College London, James D. Pollard Imperial College London, Nadesh Ramanathan Imperial College London, John Wickerson Imperial College London
DOI Pre-print File Attached
14:20
15m
Talk
Specifying and Testing GPU Workgroup Progress ModelsIn-Person
SPLASH OOPSLA
Tyler Sorensen University of California at Santa Cruz, Lucas Fernan Salvador Princeton University, Harmit Raval Princeton University, Hugues Evrard Google, John Wickerson Imperial College London, Margaret Martonosi Princeton University, Alastair F. Donaldson Imperial College London
DOI
14:35
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

18:50 - 20:10
Optimization - mirrorSPLASH OOPSLA at Zurich B
Chair(s): Tony Hosking Australian National University
18:50
15m
Talk
Copy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level Languages and BytecodeDistinguished PaperVirtual
SPLASH OOPSLA
Haoran Xu Stanford University, Fredrik Kjolstad Stanford University
DOI Pre-print
19:05
15m
Talk
VESPA: Static Profiling for Binary OptimizationVirtual
SPLASH OOPSLA
Angelica Moreira Federal University of Minas Gerais, Guilherme Ottoni Facebook, Fernando Magno Quintão Pereira Federal University of Minas Gerais
DOI
19:20
15m
Talk
A Derivative-Based Parser Generator for Visibly Pushdown GrammarsIn-Person
SPLASH OOPSLA
Xiaodong Jia Pennsylvania State University, Ashish Kumar Pennsylvania State University, Gang (Gary) Tan Pennsylvania State University
DOI
19:35
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

21:50 - 23:10
Test and Verification - mirrorSPLASH OOPSLA at Zurich B
Chair(s): Shigeru Chiba The University of Tokyo
21:50
15m
Talk
MonkeyDB: Effectively Testing Correctness under Weak Isolation LevelsDistinguished PaperVirtual
SPLASH OOPSLA
Ranadeep Biswas Informal Systems, Diptanshu Kakwani Microsoft, India, Jyothi Vedurada IIT Hyderabad, Constantin Enea University of Paris / IRIF / CNRS, Akash Lal Microsoft Research
DOI
22:05
15m
Talk
Formal Verification of High-Level SynthesisVirtual
SPLASH OOPSLA
Yann Herklotz Imperial College London, James D. Pollard Imperial College London, Nadesh Ramanathan Imperial College London, John Wickerson Imperial College London
DOI Pre-print File Attached
22:20
15m
Talk
Specifying and Testing GPU Workgroup Progress ModelsIn-Person
SPLASH OOPSLA
Tyler Sorensen University of California at Santa Cruz, Lucas Fernan Salvador Princeton University, Harmit Raval Princeton University, Hugues Evrard Google, John Wickerson Imperial College London, Margaret Martonosi Princeton University, Alastair F. Donaldson Imperial College London
DOI
22:35
35m
Live Q&A
Discussion, Questions and Answers
SPLASH OOPSLA

Sun 17 Oct

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:003020:003021:003022:003023:0030
Zurich B

Mon 18 Oct

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

Room7:00308:00309:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:003020:0030
Zurich B

Tue 19 Oct

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

Room7:00308:00309:003010:003011:003012:003013:003014:003015:003016:003017:0030
Zurich B

Wed 20 Oct

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

Fri 22 Oct

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

Room10:003011:003012:003013:003014:003015:003016:003017:003018:003019:003020:003021:003022:003023:0030
Zurich B

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 B

Mon 18 Oct

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

Room7:001530458:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:00153045
Zurich B

Tue 19 Oct

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

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 B

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 B

Fri 22 Oct

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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:0015304522:0015304523:00153045
Zurich B