SLE 2021
Sun 17 - Tue 19 October 2021
Chicago, Illinois, United States
co-located with
SPLASH 2021
Toggle navigation
Attending
Venue: Swissotel Chicago
SPLASH 2021
Venue: Online
Students
Registration
Sponsoring
Code of Conduct
Guide for Attendees
Guide for Presenters
Guide for Session Chairs and Workshop Organizers
Certificate of Attendance
Program
SLE Program
Your Program
Sun 17 Oct
Mon 18 Oct
Tue 19 Oct
Tracks
SLE 2021
SLE
Co-hosted Conferences
GPCE
Organization
SLE 2021 Committees
Track Committees
Organizing Committee
Program Committee
Artifact Evaluation Committee
Steering Committee
Contributors
People Index
Co-hosted Conferences
GPCE
Organizing Committee
Program Committee
Steering Committee
Search
Series
Series
SLE 2025
SLE 2024
SLE 2023
SLE 2022
SLE 2021
SLE 2020
SLE 2019
SLE 2018
SLE 2017
SLE 2016
SLE 2015
SLE 2013
Sign in
Sign up
SPLASH 2021
(
series
) /
SLE 2021 (
series
) /
Swissotel Chicago
/
Room information: Zurich B
Venue
Swissotel Chicago
Room name
Zurich B
Room Information
https://youtu.be/srE0WgP3JYE
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-05:00) Central Time (US & Canada)
.
Use conference time zone: (GMT-05:00) Central Time (US & Canada)
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
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 1A
SAS
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 Facts
Virtual
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 Error
Virtual
SAS
Kai Jia
Massachusetts Institute of Technology
,
Martin C. Rinard
Pre-print
09:30
15m
Talk
Verifying Low-dimensional Input Neural Networks via Input Quantization
Virtual
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 Extensions
Virtual
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 3A
SAS
at
Zurich B
+8h
Chair(s):
Mihaela Sighireanu
IRIF, Université Paris Diderot, France
13:50
15m
Talk
Static Analysis of Endian Portability by Abstract Interpretation
Virtual
SAS
David Delmas
Airbus & Sorbonne Université
,
Abdelraouf Ouadjaout
Sorbonne Université
,
Antoine Miné
Sorbonne Université
14:05
15m
Talk
Verified Functional Programming of an Abstract Interpreter
Virtual
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 Structures
Virtual
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 Answers
Virtual
SAS
15:40 - 17:00
Session 4A
SAS
at
Zurich B
Chair(s):
Cezara Drăgoi
Inria / ENS / Informal Systems
15:40
80m
Keynote
Oracle Parfait: The Flavour of Real-World Vulnerability Detection and Intelligent Configuration
Invited Talk
Virtual
SAS
Cristina Cifuentes
Oracle Labs
17:00 - 18:20
Session 1A
SAS
at
Zurich B
Chair(s):
Kedar Namjoshi
Nokia Bell Labs
17:00
15m
Talk
Accelerating Program Analyses in Datalog by Merging Library Facts
Virtual
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 Error
Virtual
SAS
Kai Jia
Massachusetts Institute of Technology
,
Martin C. Rinard
Pre-print
17:30
15m
Talk
Verifying Low-dimensional Input Neural Networks via Input Quantization
Virtual
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 Extensions
Virtual
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
21:50 - 23:10
Session 3A
SAS
at
Zurich B
Chair(s):
Suvam Mukherjee
Microsoft Research
21:50
15m
Talk
Static Analysis of Endian Portability by Abstract Interpretation
Virtual
SAS
David Delmas
Airbus & Sorbonne Université
,
Abdelraouf Ouadjaout
Sorbonne Université
,
Antoine Miné
Sorbonne Université
22:05
15m
Talk
Verified Functional Programming of an Abstract Interpreter
Virtual
SAS
Lucas Franceschino
INRIA
,
David Pichardie
Facebook Paris
,
Jean-Pierre Talpin
INRIA, France
22:30
15m
Talk
Data Abstraction: A General Framework to Handle Program Verification of Data Structures
Virtual
SAS
Julien Braine
,
Laure Gonnord
University of Lyon & LIP, France
,
David Monniaux
CNRS/VERIMAG
22:45
25m
Live Q&A
Session 3A Discussion, Questions and Answers
Virtual
SAS
Mon 18 Oct
Displayed time zone:
Central Time (US & Canada)
change
07:40 - 09:00
Session 4B
SAS
at
Zurich B
Chair(s):
Antoine Miné
Sorbonne Université
07:40
15m
Talk
Automated Verification of the Parallel Bellman--Ford Algorithm
Virtual
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 Folding
Virtual
SAS
Marek Chalupa
Masaryk University
,
Jan Strejcek
Masaryk University
08:10
15m
Talk
Improving Thread-Modular Abstract Interpretation
Virtual
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 Solving
Virtual
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 2B
SAS
at
Zurich B
+8h
Chair(s):
Cezara Drăgoi
Inria / ENS / Informal Systems
10:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication Abstraction
Virtual
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 Bounding
Virtual
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 Concurrency
Virtual
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 3B
SAS
at
Zurich B
Chair(s):
Kedar Namjoshi
Nokia Bell Labs
13:50
80m
Keynote
Interactive Code Analysis
Invited Talk
Virtual
SAS
I:
Gerard Holzmann
NASA/Caltech Jet Propulsion Laboratory
15:40 - 17:00
Session 4B
SAS
at
Zurich B
-8h
Chair(s):
Kedar Namjoshi
Nokia Bell Labs
15:40
15m
Talk
Automated Verification of the Parallel Bellman--Ford Algorithm
Virtual
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 Folding
Virtual
SAS
Marek Chalupa
Masaryk University
,
Jan Strejcek
Masaryk University
16:10
15m
Talk
Improving Thread-Modular Abstract Interpretation
Virtual
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 Solving
Virtual
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 2B
SAS
at
Zurich B
Chair(s):
Suvam Mukherjee
Microsoft Research
18:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication Abstraction
Virtual
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 Bounding
Virtual
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 Concurrency
Virtual
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
Education
SPLASH REBASE
at
Zurich B
07:30
90m
Talk
Hedy: Creating a gradual programming language
Virtual
SPLASH REBASE
Felienne Hermans
Leiden University
,
Federico Tomassetti
Independent
09:00 - 10:30
Dynamism
SPLASH REBASE
at
Zurich B
09:00
90m
Talk
The F# view on the Static / Dynamic divide
Virtual
SPLASH REBASE
Don Syme
Microsoft
,
Nicholas Matsakis
Amazon, USA
10:50 - 12:20
Language
SPLASH REBASE
at
Zurich B
10:50
90m
Talk
A Retrospective on the Design of the Swift Programming Language
Virtual
SPLASH REBASE
Dave Abrahams
Adobe
,
Roman Elizarov
JetBrains
,
Denys Shabalin
Google
13:50 - 15:20
Interfaces
SPLASH REBASE
at
Zurich B
13:50
90m
Talk
A Brief History of the API, Revisited
Virtual
SPLASH REBASE
Josh Bloch
Carnegie Mellon University
,
Doug Lea
State University of New York (SUNY) Oswego
15:40 - 17:10
Hardware
SPLASH REBASE
at
Zurich B
15:40
90m
Talk
Fragmentation of Machine Architecture
Virtual
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 - mirror
SPLASH 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 Programming
Virtual
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 Systems
In-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 APIs
In-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 Systems
In-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
Testing
SPLASH 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 Bugs
Virtual
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 Typestate
Virtual
SPLASH OOPSLA
Karl Cronburg
Tufts University
,
Sam Guyer
Tufts University
DOI
Pre-print
11:20
15m
Talk
Generative Type-Aware Mutation for Testing SMT Solvers
Virtual
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 Testing
In-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 1
SPLASH Faculty Mentorship Roundtable
at
Zurich B
Chair(s):
Danny Dig
University of Colorado Boulder, USA
12:10
1h40m
Meeting
Faculty Mentoring Roundtable
In-Person
SPLASH Faculty Mentorship Roundtable
13:50 - 15:10
Security
SPLASH OOPSLA
at
Zurich B
+8h
Chair(s):
Yannis Smaragdakis
University of Athens
13:50
15m
Talk
SpecSafe: Detecting Cache Side Channels in a Speculative World
Virtual
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 Designs
Virtual
SPLASH OOPSLA
Ziqiao Zhou
Microsoft Research
,
Michael K. Reiter
Duke University
DOI
14:20
15m
Talk
Reconciling Optimization with Secure Compilation
Virtual
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 Sets
In-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 Programming
SPLASH 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 Programming
Virtual
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 Systems
In-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 APIs
In-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 Systems
In-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
Reception
SPLASH Opening
at
Zurich B
17:00
1h50m
Other
Reception
In-Person
SPLASH Opening
18:50 - 20:10
Testing - Mirror
SPLASH 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 Bugs
Virtual
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 Typestate
Virtual
SPLASH OOPSLA
Karl Cronburg
Tufts University
,
Sam Guyer
Tufts University
DOI
Pre-print
19:20
15m
Talk
Generative Type-Aware Mutation for Testing SMT Solvers
Virtual
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 Testing
In-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 - mirror
SPLASH OOPSLA
at
Zurich B
Chair(s):
Chandrakana Nandi
Certora, inc.
21:50
15m
Talk
SpecSafe: Detecting Cache Side Channels in a Speculative World
Virtual
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 Designs
Virtual
SPLASH OOPSLA
Ziqiao Zhou
Microsoft Research
,
Michael K. Reiter
Duke University
DOI
22:20
15m
Talk
Reconciling Optimization with Secure Compilation
Virtual
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 Sets
In-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 - mirror
SPLASH OOPSLA
at
Zurich B
Chair(s):
Patrick Eugster
USI Lugano; Purdue University
07:40
15m
Talk
Rich Specifications for Ethereum Smart Contract Verification
Virtual
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 Contracts
Virtual
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 Code
Virtual
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 Serverless
In-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 Languages
SPLASH OOPSLA
at
Zurich B
+8h
Chair(s):
Julia Belyakova
Northeastern University
10:50
15m
Talk
Gradually Structured Data
Virtual
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 Migration
Virtual
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 Prediction
Virtual
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 Semantics
In-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 2
SPLASH Faculty Mentorship Roundtable
at
Zurich B
Chair(s):
Danny Dig
University of Colorado Boulder, USA
12:10
1h40m
Meeting
Faculty Mentoring Roundtable
In-Person
SPLASH Faculty Mentorship Roundtable
13:50 - 15:10
Program Synthesis
SPLASH OOPSLA
at
Zurich B
+8h
Chair(s):
Kedar Namjoshi
Nokia Bell Labs
13:50
15m
Talk
Generalizable Synthesis through Unification
Virtual
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 Graphs
Virtual
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 Libraries
Virtual
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 Structures
Virtual
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 Programming
SPLASH OOPSLA
at
Zurich B
-8h
Chair(s):
Mohsen Lesani
University of California at Riverside
15:40
15m
Talk
Rich Specifications for Ethereum Smart Contract Verification
Virtual
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 Contracts
Virtual
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 Code
Virtual
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 Serverless
In-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
Reception
SPLASH Opening
at
Zurich B
17:00
1h50m
Other
Reception
In-Person
SPLASH Opening
18:50 - 20:10
Dynamic Languages - mirror
SPLASH OOPSLA
at
Zurich B
Chair(s):
Julia Belyakova
Northeastern University
18:50
15m
Talk
Gradually Structured Data
Virtual
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 Migration
Virtual
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 Prediction
Virtual
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 Semantics
In-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 - mirror
SPLASH OOPSLA
at
Zurich B
Chair(s):
Hakjoo Oh
Korea University
21:50
15m
Talk
Generalizable Synthesis through Unification
Virtual
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 Graphs
Virtual
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 Libraries
Virtual
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 Structures
Virtual
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
Optimization
SPLASH 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 Bytecode
Virtual
SPLASH OOPSLA
Haoran Xu
Stanford University
,
Fredrik Kjolstad
Stanford University
DOI
Pre-print
11:05
15m
Talk
VESPA: Static Profiling for Binary Optimization
Virtual
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 Grammars
In-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 Verification
SPLASH OOPSLA
at
Zurich B
+8h
Chair(s):
Mike Dodds
Galois, Inc.
13:50
15m
Talk
MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
Virtual
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 Synthesis
Virtual
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 Models
In-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 - mirror
SPLASH 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 Bytecode
Virtual
SPLASH OOPSLA
Haoran Xu
Stanford University
,
Fredrik Kjolstad
Stanford University
DOI
Pre-print
19:05
15m
Talk
VESPA: Static Profiling for Binary Optimization
Virtual
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 Grammars
In-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 - mirror
SPLASH OOPSLA
at
Zurich B
Chair(s):
Shigeru Chiba
The University of Tokyo
21:50
15m
Talk
MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
Virtual
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 Synthesis
Virtual
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 Models
In-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
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
19:00
30
20:00
30
21:00
30
22:00
30
23:00
30
Zurich B
SAS
Session 1A
SPLASH Ask Me Anything (AMA)
SAS
SAS
Session 3A
SAS
Session 4A
SAS
Session 1A
SAS
SAS
Session 3A
Mon 18 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
7:00
30
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
19:00
30
20:00
30
Zurich B
SAS
Session 4B
SAS
SAS
Session 2B
SAS
Session 3B
SAS
Session 4B
SAS
SAS
Session 2B
Tue 19 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
7:00
30
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Zurich B
SPLASH REBASE
Education
SPLASH REBASE
Dynamism
SPLASH REBASE
Language
SPLASH REBASE
Interfaces
SPLASH REBASE
Hardware
Wed 20 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
7:00
30
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
19:00
30
20:00
30
21:00
30
22:00
30
23:00
30
Zurich B
SPLASH OOPSLA
Distributed Programming - mirror
SPLASH OOPSLA
Testing
SPLASH Faculty Mentorship Roundtable
Session 1
SPLASH OOPSLA
Security
SPLASH OOPSLA
Distributed Programming
SPLASH Opening
Reception
SPLASH OOPSLA
Testing - Mirror
SPLASH OOPSLA
Security - mirror
Thu 21 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
7:00
30
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
19:00
30
20:00
30
21:00
30
22:00
30
23:00
30
Zurich B
SPLASH OOPSLA
Smart Contracts and Distributed Programming - mirror
SPLASH OOPSLA
Dynamic Languages
SPLASH Faculty Mentorship Roundtable
Session 2
SPLASH OOPSLA
Program Synthesis
SPLASH OOPSLA
Smart Contracts and Distributed Programming
SPLASH Opening
Reception
SPLASH OOPSLA
Dynamic Languages - mirror
SPLASH OOPSLA
Program Synthesis - mirror
Fri 22 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
19:00
30
20:00
30
21:00
30
22:00
30
23:00
30
Zurich B
SPLASH OOPSLA
Optimization
SPLASH OOPSLA
Test and Verification
SPLASH OOPSLA
Optimization - mirror
SPLASH OOPSLA
Test and Verification - mirror
Sun 17 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
21:00
15
30
45
22:00
15
30
45
23:00
15
30
45
Zurich B
SAS
Virtual
Accelerating Program Analyses in Datalog by Merging Library Facts
09:00 - 09:15
SAS
Virtual
Exploiting Verified Neural Networks via Floating Point Numerical Error
09:15 - 09:30
SAS
Virtual
Verifying Low-dimensional Input Neural Networks via Input Quantization
09:30 - 09:45
SAS
Virtual
A Multi-Language Static Analysis of Python Programs with Native C Exten ...
09:45 - 10:00
SAS
Virtual
Session 1A Discussion, Questions and Answers
10:00 - 10:20
SAS
Virtual
Static Analysis of Endian Portability by Abstract Interpretation
13:50 - 14:05
SAS
Virtual
Verified Functional Programming of an Abstract Interpreter
14:05 - 14:20
SAS
Virtual
Data Abstraction: A General Framework to Handle Program Verification of ...
14:30 - 14:45
SAS
Virtual
Session 3A Discussion, Questions and Answers
14:45 - 15:10
SAS
Invited Talk
Virtual
Oracle Parfait: The Flavour of Real-World Vulnerability Detection and I ...
15:40 - 17:00
SAS
Virtual
Accelerating Program Analyses in Datalog by Merging Library Facts
17:00 - 17:15
SAS
Virtual
Exploiting Verified Neural Networks via Floating Point Numerical Error
17:15 - 17:30
SAS
Virtual
Verifying Low-dimensional Input Neural Networks via Input Quantization
17:30 - 17:45
SAS
Virtual
A Multi-Language Static Analysis of Python Programs with Native C Exten ...
17:45 - 18:00
SAS
Virtual
Session 1A Discussion, Questions and Answers
18:00 - 18:20
SAS
Virtual
Static Analysis of Endian Portability by Abstract Interpretation
21:50 - 22:05
SAS
Virtual
Verified Functional Programming of an Abstract Interpreter
22:05 - 22:20
SAS
Virtual
Data Abstraction: A General Framework to Handle Program Verification of ...
22:30 - 22:45
SAS
Virtual
Session 3A Discussion, Questions and Answers
22:45 - 23:10
Mon 18 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
7:00
15
30
45
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
Zurich B
SAS
Virtual
Automated Verification of the Parallel Bellman--Ford Algorithm
07:40 - 07:55
SAS
Virtual
Backward Symbolic Execution with Loop Folding
07:55 - 08:10
SAS
Virtual
Improving Thread-Modular Abstract Interpretation
08:10 - 08:25
SAS
Virtual
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
08:25 - 08:40
SAS
Session 4B Discussion, Questions and Answers
08:40 - 09:00
SAS
Virtual
Compositional Verification of Smart Contracts Through Communication Abs ...
10:50 - 11:05
SAS
Virtual
Selectively-Amortized Resource Bounding
11:05 - 11:20
SAS
Virtual
Thread-modular Analysis of Release-Acquire Concurrency
11:20 - 11:35
SAS
Session 2B Discussion, Questions and Answers
11:35 - 12:10
SAS
Invited Talk
Virtual
Interactive Code Analysis
13:50 - 15:10
SAS
Virtual
Automated Verification of the Parallel Bellman--Ford Algorithm
15:40 - 15:55
SAS
Virtual
Backward Symbolic Execution with Loop Folding
15:55 - 16:10
SAS
Virtual
Improving Thread-Modular Abstract Interpretation
16:10 - 16:25
SAS
Virtual
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
16:25 - 16:40
SAS
Session 4B Discussion, Questions and Answers
16:40 - 17:00
SAS
Virtual
Compositional Verification of Smart Contracts Through Communication Abs ...
18:50 - 19:05
SAS
Virtual
Selectively-Amortized Resource Bounding
19:05 - 19:20
SAS
Virtual
Thread-modular Analysis of Release-Acquire Concurrency
19:20 - 19:35
SAS
Session 2B Discussion, Questions and Answers
19:35 - 20:10
Tue 19 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
7:00
15
30
45
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Zurich B
SPLASH REBASE
Virtual
Hedy: Creating a gradual programming language
07:30 - 09:00
SPLASH REBASE
Virtual
The F# view on the Static / Dynamic divide
09:00 - 10:30
SPLASH REBASE
Virtual
A Retrospective on the Design of the Swift Programming Language
10:50 - 12:20
SPLASH REBASE
Virtual
A Brief History of the API, Revisited
13:50 - 15:20
SPLASH REBASE
Virtual
Fragmentation of Machine Architecture
15:40 - 17:10
Wed 20 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
7:00
15
30
45
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
21:00
15
30
45
22:00
15
30
45
23:00
15
30
45
Zurich B
SPLASH OOPSLA
Virtual
A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven ...
07:40 - 07:55
SPLASH OOPSLA
In-Person
Much ADO about Failures: A Fault-Aware Model for Compositional Verifica ...
07:55 - 08:10
SPLASH OOPSLA
In-Person
Automatic Migration from Synchronous to Asynchronous JavaScript APIs
08:10 - 08:25
SPLASH OOPSLA
In-Person
QuickSilver: Modeling and Parameterized Verification for Distributed Ag ...
08:25 - 08:40
SPLASH OOPSLA
Discussion, Questions and Answers
08:40 - 09:00
SPLASH OOPSLA
Virtual
Fully Automated Functional Fuzzing of Android Apps for Detecting Non-cr ...
10:50 - 11:05
SPLASH OOPSLA
Virtual
Permchecker: A Toolchain for Debugging Memory Managers with Typestate
11:05 - 11:20
SPLASH OOPSLA
Virtual
Generative Type-Aware Mutation for Testing SMT Solvers
11:20 - 11:35
SPLASH OOPSLA
In-Person
Programming and Execution Models for Parallel Bounded Exhaustive Testing
11:35 - 11:50
SPLASH OOPSLA
Discussion, Questions and Answers
11:50 - 12:10
SPLASH Faculty Mentorship Roundtable
In-Person
Faculty Mentoring Roundtable
12:10 - 13:50
SPLASH OOPSLA
Virtual
SpecSafe: Detecting Cache Side Channels in a Speculative World
13:50 - 14:05
SPLASH OOPSLA
Virtual
Interpretable Noninterference Measurement and Its Application to Proces ...
14:05 - 14:20
SPLASH OOPSLA
Virtual
Reconciling Optimization with Secure Compilation
14:20 - 14:35
SPLASH OOPSLA
In-Person
Not So Fast: Understanding and Mitigating Negative Impacts of Compiler ...
14:35 - 14:50
SPLASH OOPSLA
Discussion, Questions and Answers
14:50 - 15:10
SPLASH OOPSLA
Virtual
A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven ...
15:40 - 15:55
SPLASH OOPSLA
In-Person
Much ADO about Failures: A Fault-Aware Model for Compositional Verifica ...
15:55 - 16:10
SPLASH OOPSLA
In-Person
Automatic Migration from Synchronous to Asynchronous JavaScript APIs
16:10 - 16:25
SPLASH OOPSLA
In-Person
QuickSilver: Modeling and Parameterized Verification for Distributed Ag ...
16:25 - 16:40
SPLASH OOPSLA
Discussion, Questions and Answers
16:40 - 17:00
SPLASH Opening
In-Person
Reception
17:00 - 18:50
SPLASH OOPSLA
Virtual
Fully Automated Functional Fuzzing of Android Apps for Detecting Non-cr ...
18:50 - 19:05
SPLASH OOPSLA
Virtual
Permchecker: A Toolchain for Debugging Memory Managers with Typestate
19:05 - 19:20
SPLASH OOPSLA
Virtual
Generative Type-Aware Mutation for Testing SMT Solvers
19:20 - 19:35
SPLASH OOPSLA
In-Person
Programming and Execution Models for Parallel Bounded Exhaustive Testing
19:35 - 19:50
SPLASH OOPSLA
Discussion, Questions and Answers
19:50 - 20:10
SPLASH OOPSLA
Virtual
SpecSafe: Detecting Cache Side Channels in a Speculative World
21:50 - 22:05
SPLASH OOPSLA
Virtual
Interpretable Noninterference Measurement and Its Application to Proces ...
22:05 - 22:20
SPLASH OOPSLA
Virtual
Reconciling Optimization with Secure Compilation
22:20 - 22:35
SPLASH OOPSLA
In-Person
Not So Fast: Understanding and Mitigating Negative Impacts of Compiler ...
22:35 - 22:50
SPLASH OOPSLA
Discussion, Questions and Answers
22:50 - 23:10
Thu 21 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
7:00
15
30
45
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
21:00
15
30
45
22:00
15
30
45
23:00
15
30
45
Zurich B
SPLASH OOPSLA
Virtual
Rich Specifications for Ethereum Smart Contract Verification
07:40 - 07:55
SPLASH OOPSLA
Virtual
Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling o ...
07:55 - 08:10
SPLASH OOPSLA
Virtual
ECROs: Building Global Scale Systems from Sequential Code
08:10 - 08:25
SPLASH OOPSLA
In-Person
Durable Functions: Semantics for Stateful Serverless
08:25 - 08:40
SPLASH OOPSLA
Discussion, Questions and Answers
08:40 - 09:00
SPLASH OOPSLA
Virtual
Gradually Structured Data
10:50 - 11:05
SPLASH OOPSLA
Virtual
Solver-Based Gradual Type Migration
11:05 - 11:20
SPLASH OOPSLA
Virtual
SimTyper: Sound Type Inference for Ruby using Type Equality Prediction
11:20 - 11:35
SPLASH OOPSLA
In-Person
Promises Are Made to Be Broken: Migrating R to Strict Semantics
11:35 - 11:50
SPLASH OOPSLA
Discussion, Questions and Answers
11:50 - 12:10
SPLASH Faculty Mentorship Roundtable
In-Person
Faculty Mentoring Roundtable
12:10 - 13:50
SPLASH OOPSLA
Virtual
Generalizable Synthesis through Unification
13:50 - 14:05
SPLASH OOPSLA
Virtual
Gauss: Program Synthesis by Reasoning over Graphs
14:05 - 14:20
SPLASH OOPSLA
Virtual
APIfix: Output-Oriented Program Synthesis for Combating Breaking Change ...
14:20 - 14:35
SPLASH OOPSLA
Virtual
LooPy: Interactive Program Synthesis with Control Structures
14:35 - 14:50
SPLASH OOPSLA
Discussion, Questions and Answers
14:50 - 15:10
SPLASH OOPSLA
Virtual
Rich Specifications for Ethereum Smart Contract Verification
15:40 - 15:55
SPLASH OOPSLA
Virtual
Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling o ...
15:55 - 16:10
SPLASH OOPSLA
Virtual
ECROs: Building Global Scale Systems from Sequential Code
16:10 - 16:25
SPLASH OOPSLA
In-Person
Durable Functions: Semantics for Stateful Serverless
16:25 - 16:40
SPLASH OOPSLA
Discussion, Questions and Answers
16:40 - 17:00
SPLASH Opening
In-Person
Reception
17:00 - 18:50
SPLASH OOPSLA
Virtual
Gradually Structured Data
18:50 - 19:05
SPLASH OOPSLA
Virtual
Solver-Based Gradual Type Migration
19:05 - 19:20
SPLASH OOPSLA
Virtual
SimTyper: Sound Type Inference for Ruby using Type Equality Prediction
19:20 - 19:35
SPLASH OOPSLA
In-Person
Promises Are Made to Be Broken: Migrating R to Strict Semantics
19:35 - 19:50
SPLASH OOPSLA
Discussion, Questions and Answers
19:50 - 20:10
SPLASH OOPSLA
Virtual
Generalizable Synthesis through Unification
21:50 - 22:05
SPLASH OOPSLA
Virtual
Gauss: Program Synthesis by Reasoning over Graphs
22:05 - 22:20
SPLASH OOPSLA
Virtual
APIfix: Output-Oriented Program Synthesis for Combating Breaking Change ...
22:20 - 22:35
SPLASH OOPSLA
Virtual
LooPy: Interactive Program Synthesis with Control Structures
22:35 - 22:50
SPLASH OOPSLA
Discussion, Questions and Answers
22:50 - 23:10
Fri 22 Oct
Displayed time zone:
Central Time (US & Canada)
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
21:00
15
30
45
22:00
15
30
45
23:00
15
30
45
Zurich B
SPLASH OOPSLA
Virtual
Copy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level ...
10:50 - 11:05
SPLASH OOPSLA
Virtual
VESPA: Static Profiling for Binary Optimization
11:05 - 11:20
SPLASH OOPSLA
In-Person
A Derivative-Based Parser Generator for Visibly Pushdown Grammars
11:20 - 11:35
SPLASH OOPSLA
Discussion, Questions and Answers
11:35 - 12:10
SPLASH OOPSLA
Virtual
MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
13:50 - 14:05
SPLASH OOPSLA
Virtual
Formal Verification of High-Level Synthesis
14:05 - 14:20
SPLASH OOPSLA
In-Person
Specifying and Testing GPU Workgroup Progress Models
14:20 - 14:35
SPLASH OOPSLA
Discussion, Questions and Answers
14:35 - 15:10
SPLASH OOPSLA
Virtual
Copy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level ...
18:50 - 19:05
SPLASH OOPSLA
Virtual
VESPA: Static Profiling for Binary Optimization
19:05 - 19:20
SPLASH OOPSLA
In-Person
A Derivative-Based Parser Generator for Visibly Pushdown Grammars
19:20 - 19:35
SPLASH OOPSLA
Discussion, Questions and Answers
19:35 - 20:10
SPLASH OOPSLA
Virtual
MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
21:50 - 22:05
SPLASH OOPSLA
Virtual
Formal Verification of High-Level Synthesis
22:05 - 22:20
SPLASH OOPSLA
In-Person
Specifying and Testing GPU Workgroup Progress Models
22:20 - 22:35
SPLASH OOPSLA
Discussion, Questions and Answers
22:35 - 23:10
x
Sat 21 Dec 18:14