Program - SPLASH 2021

Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States

Main Program Workshops and Co-located Events Detailed Table Session Timeline Detailed Timeline

The Main Program view shows a partial program, use other views for the complete program.

Get Calendar (iCal)

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

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 programSpecify a time band

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

Sun 17 Oct

7:40

A Concurrency Model for JavaScript with Cooperative Cancellation

Tian Zhao, Yonglun Li

There Is More Than One Way to Zen Your Python

Aamir Farooq, Vadim Zaytsev

8:00

Getting Grammars into Shape for Block-based Editors

Mauricio Verano Merino, Tom Beckmann, Tijs van der Storm, Robert Hirschfeld, Jurgen Vinju

8:20

Extracting The Power of Dependent Types

Artjoms Šinkarovs, Jesper Cockx

8:40

Discussion, Questions, Answers

9:00

+8h Solidifying and Advancing the Software Foundations

+8hAccelerating Program Analyses in Datalog by Merging Library Facts

Yifan Chen, Chenyang Yang, Xin Zhang, Yingfei Xiong, Hao Tang, Xiaoyin Wang, Lu Zhang

+8hSLE/GPCE Joint Welcome

Coen De Roover, Emma Söderberg, Dimitris Kolovos

+8hExploiting Verified Neural Networks via Floating Point Numerical Error

Kai Jia, Martin C. Rinard

9:20

+8hSLE Keynote - Integrating Usability into Programming Language Design

Jonathan Aldrich

In-PersonKeynote

+8hVerifying Low-dimensional Input Neural Networks via Input Quantization

Kai Jia, Martin C. Rinard

9:40

+8hA Multi-Language Static Analysis of Python Programs with Native C Extensions

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné

+8hMonilogging for Executable Domain-Specific Languages

Dorian Leroy, Benoît Lelandais, Marie-Pierre Oudot, Benoit Combemale

10:00

+8hSession 1A Discussion, Questions and Answers

+8hVision: The Next 700 Language Workbenches

+8hDiscussion, Questions, Answers

10:20

10:40

+8hScalable and Modular Robustness Analysis of Deep Neural Networks

Yuyi Zhong, Quang-Trung Ta, Tianzuo Luo, Fanlong ZHANG, Siau-Cheng Khoo

+8hGPCE Keynote - Live Programming and Programming by Example: Better Together

11:00

+8hServer-Side Computation of Package Dependencies in Package-Management Systems

Nobuhiro Kasai, Isao Sasano

11:20

+8hPyCT: A Python Concolic Tester

Wei-Lun Tsai, Wei-Cheng Wu, Di-De Yen, Fang Yu, Yu-Fang Chen

+8hAutomating the Synthesis of Recommender Systems for Modelling Languages

Lissette Almonte, Sara Perez-Soler, Esther Guerra, Iván Cantador, Juan de Lara

+8hProgram Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications

Wonhyuk Choi, Michel Vazirani, Mark Santolucito

+8hExecuting Certified Model Transformations on Apache Spark

Jolan Philippe, Massimo Tisi, Hélène Coullon, Gerson Sunyé

11:40

+8hFunction Pointer Eliminator for C Programs

Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, Koji Nakazawa

+8hQ&A and discussion

+8hNew Ideas: Automated Engineering of Metamorphic Testing Environments for Domain-Specific Languages

Pablo C Canizares, Pablo Gómez-Abajo, Alberto Núňez, Esther Guerra, Juan de Lara

12:00

+8hDiscussion, Questions, Answers

12:20

12:40

13:00

13:20

13:40

+8hA Dictionary-Passing Translation of Featherweight Go

Martin Sulzmann, Stefan Wehr

+8hStatic Analysis of Endian Portability by Abstract Interpretation

David Delmas, Abdelraouf Ouadjaout, Antoine Miné

+8hA Variational Database Management System

Parisa Ataei, Fariba Khan, Eric Walkingshaw

14:00

+8hA compilation method for dynamic typing in ML

Atsushi Ohori, Katsuhiro Ueno

+8hVerified Functional Programming of an Abstract Interpreter

Lucas Franceschino, David Pichardie, Jean-Pierre Talpin

+8hThe Life Cycle of Features in Highly-Configurable Software Systems Evolving in Space and Time

Gabriela Karoline Michelon, Wesley Assunção, David Obermann, Lukas Linsbauer, Paul Grünbacher, Alexander Egyed

14:20

+8hFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly

Carmine Abate, Matteo Busi, Stelios Tsampas

+8hTowards Supporting SPL Engineering in Low-Code Platforms using a DSL Approach

Alexandre Bragança, Isabel Azevedo, Nuno Bettencourt, Carlos Morais, Diogo Teixeira, David Caetano

+8hData Abstraction: A General Framework to Handle Program Verification of Data Structures

Julien Braine, Laure Gonnord, David Monniaux

+8hHybrid quantum-classical circuit simplification with the ZX-calculus

Agustín Borgna, Simon Perdrix, Benoit Valiron

+8hOn-Stack Replacement for Program Generators and Source-to-Source Compilers

Gregory Essertel, Ruby Tahboub, Tiark Rompf

14:40

+8hSession 3A Discussion, Questions and Answers

+8hQ&A and discussion

+8hDiscussion, Questions, Answers

15:00

15:20

15:40

Oracle Parfait: The Flavour of Real-World Vulnerability Detection and Intelligent Configuration

Cristina Cifuentes

Invited TalkVirtual

-8hA Concurrency Model for JavaScript with Cooperative Cancellation

Tian Zhao, Yonglun Li

-8hThere Is More Than One Way to Zen Your Python

Aamir Farooq, Vadim Zaytsev

16:00

-8hGetting Grammars into Shape for Block-based Editors

Mauricio Verano Merino, Tom Beckmann, Tijs van der Storm, Robert Hirschfeld, Jurgen Vinju

16:20

-8hExtracting The Power of Dependent Types

Artjoms Šinkarovs, Jesper Cockx

16:40

-8hDiscussion, Questions, Answers

17:00

Solidifying and Advancing the Software Foundations

Accelerating Program Analyses in Datalog by Merging Library Facts

Yifan Chen, Chenyang Yang, Xin Zhang, Yingfei Xiong, Hao Tang, Xiaoyin Wang, Lu Zhang

SLE/GPCE Joint Welcome

Coen De Roover, Emma Söderberg, Dimitris Kolovos

Exploiting Verified Neural Networks via Floating Point Numerical Error

Kai Jia, Martin C. Rinard

17:20

SLE Keynote - Integrating Usability into Programming Language Design

Jonathan Aldrich

In-PersonKeynote

Verifying Low-dimensional Input Neural Networks via Input Quantization

Kai Jia, Martin C. Rinard

17:40

A Multi-Language Static Analysis of Python Programs with Native C Extensions

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné

Monilogging for Executable Domain-Specific Languages

Dorian Leroy, Benoît Lelandais, Marie-Pierre Oudot, Benoit Combemale

18:00

Session 1A Discussion, Questions and Answers

Vision: The Next 700 Language Workbenches

Discussion, Questions, Answers

18:20

18:40

Scalable and Modular Robustness Analysis of Deep Neural Networks

Yuyi Zhong, Quang-Trung Ta, Tianzuo Luo, Fanlong ZHANG, Siau-Cheng Khoo

GPCE Keynote - Live Programming and Programming by Example: Better Together

19:00

Server-Side Computation of Package Dependencies in Package-Management Systems

Nobuhiro Kasai, Isao Sasano

19:20

PyCT: A Python Concolic Tester

Wei-Lun Tsai, Wei-Cheng Wu, Di-De Yen, Fang Yu, Yu-Fang Chen

Automating the Synthesis of Recommender Systems for Modelling Languages

Lissette Almonte, Sara Perez-Soler, Esther Guerra, Iván Cantador, Juan de Lara

Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications

Wonhyuk Choi, Michel Vazirani, Mark Santolucito

Executing Certified Model Transformations on Apache Spark

Jolan Philippe, Massimo Tisi, Hélène Coullon, Gerson Sunyé

19:40

Function Pointer Eliminator for C Programs

Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, Koji Nakazawa

Q&A and discussion

New Ideas: Automated Engineering of Metamorphic Testing Environments for Domain-Specific Languages

Pablo C Canizares, Pablo Gómez-Abajo, Alberto Núňez, Esther Guerra, Juan de Lara

20:00

Discussion, Questions, Answers

20:20

20:40

21:00

21:20

21:40

A Dictionary-Passing Translation of Featherweight Go

Martin Sulzmann, Stefan Wehr

Static Analysis of Endian Portability by Abstract Interpretation

David Delmas, Abdelraouf Ouadjaout, Antoine Miné

A Variational Database Management System

Parisa Ataei, Fariba Khan, Eric Walkingshaw

22:00

A compilation method for dynamic typing in ML

Atsushi Ohori, Katsuhiro Ueno

Verified Functional Programming of an Abstract Interpreter

Lucas Franceschino, David Pichardie, Jean-Pierre Talpin

The Life Cycle of Features in Highly-Configurable Software Systems Evolving in Space and Time

Gabriela Karoline Michelon, Wesley Assunção, David Obermann, Lukas Linsbauer, Paul Grünbacher, Alexander Egyed

22:20

Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly

Carmine Abate, Matteo Busi, Stelios Tsampas

Towards Supporting SPL Engineering in Low-Code Platforms using a DSL Approach

Alexandre Bragança, Isabel Azevedo, Nuno Bettencourt, Carlos Morais, Diogo Teixeira, David Caetano

Data Abstraction: A General Framework to Handle Program Verification of Data Structures

Julien Braine, Laure Gonnord, David Monniaux

Hybrid quantum-classical circuit simplification with the ZX-calculus

Agustín Borgna, Simon Perdrix, Benoit Valiron

On-Stack Replacement for Program Generators and Source-to-Source Compilers

Gregory Essertel, Ruby Tahboub, Tiark Rompf

22:40

Session 3A Discussion, Questions and Answers

Q&A and discussion

Discussion, Questions, Answers

23:00

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

Mon 18 Oct

7:40

Automated Verification of the Parallel Bellman--Ford Algorithm

Mohsen Safari, Wytse Oortwijn, Marieke Huisman

Leveraging Relational Concept Analysis for Automated Feature Location in Software Product Lines

Nicolas Hlad, Bérénice Lemoine, Marianne Huchard, Abdelhak Seriai

Backward Symbolic Execution with Loop Folding

Marek Chalupa, Jan Strejcek

FIDDLR: Streamlining Reuse with Concern-Specific Modelling Languages

Maximilian Schiedermeier, Jörg Kienzle, Bettina Kemme

8:00

Improving Thread-Modular Abstract Interpretation

Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani

Lifted Termination Analysis by Abstract Interpretation and its Applications

Aleksandar S. Dimovski

8:20

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving

Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

Delta-based Verification of Software Product Families

Marco Scaletta, Reiner Hähnle, Dominic Steinhöfel, Richard Bubel

8:40

Session 4B Discussion, Questions and Answers

Discussion, Questions and Answers

9:00

+8hA Separation Logic for Probabilistic Independence

+8hType-safe generation of modules in applicative and generative styles

Yuhi Sato, Yukiyoshi Kameyama

+8hHACCLE: Metaprogramming for Secure Multi-Party Computation

Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Nouraldin Jaber, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoit Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni

9:20

+8hMulti-Stage Programming with Generative and Analytical Macros

Nicolas Stucki, Jonathan Immanuel Brachthäuser, Martin Odersky

VirtualGPCE Best Paper Award

9:40

+8hMetaprogramming with Combinators

Mahshid Shahmohammadian, Geoffrey Mainland

10:00

+8hDiscussion, Questions and Answers

10:20

Invited Speaker

10:40

+8hA Typed Programmatic Interface to Contracts on the Blockchain

Thi Thu Ha Doan, Peter Thiemann

+8hCompositional Verification of Smart Contracts Through Communication Abstraction

Scott Wesley, Maria Christakis, Arie Gurfinkel, Jorge A. Navas, Richard Trefler, Valentin Wüstholz

+8hFast Incremental PEG Parsing

Zachary Yedidia, Stephen Chong

11:00

+8hAdaptable Traces for Program Explanations

Divya Bajaj, Martin Erwig, Danila Fedorin, Kai Gay

+8hSelectively-Amortized Resource Bounding

Tianhan Lu, Bor-Yuh Evan Chang, Ashutosh Trivedi

+8hFaster Reachability Analysis for LR(1) Parsers

Frédéric Bour, François Pottier

11:20

+8hLatent Effects for Reusable Language Components

Birthe van den Berg, Casper Bach Poulsen, Tom Schrijvers, Nicolas Wu

+8hThread-modular Analysis of Release-Acquire Concurrency

Divyanjali Sharma, Subodh Sharma

+8hAutomatic Grammar Repair

Moeketsi Raselimo, Bernd Fischer

+8hThe Choice Construct in the Soufflé Language

Xiaowen Hu, Joshua Karp, David Zhao, Abdul Zreika, Xi Wu, Bernhard Scholz

+8hSession 2B Discussion, Questions and Answers

+8hVision: Bias in Systematic Grammar-Based Test Suite Construction Algorithms

Christoff Rossouw, Bernd Fischer

11:40

+8hCompiling pattern matching to in-place modifications

+8hQ&A and discussion

+8hDiscussion, Questions and Answers

12:00

12:20

12:40

13:00

13:20

13:40

+8hPreprocessing of Alternating Automata for Language Emptiness Testing

Pavol Vargovčík, Lukáš Holík

Interactive Code Analysis

Gerard Holzmann

Invited TalkVirtual

+8hA DSL for Explanatory Decision Making

Martin Erwig, Prashant Kumar

14:00

+8hProving LTL Properties of Bitvector Programs and Decompiled Binaries

Cyrus Liu, Chengbin Pang, Daniel Dietsch, Eric Koskinen, Ton Chanh Le, Georgios Portokalidis, Jun Xu

+8hSEALS: A framework for building Self-Adaptive Virtual Machines

Gwendal Jouneaux, Olivier Barais, Benoit Combemale, Gunter Mussbacher

14:20

+8hSolving Not-Substring with Flat Abstraction

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, Di-De Yen

+8hUnderstanding and Improving Model-Driven IoT Systems Through Accompanying Digital Twins

Jörg Christian Kirchhof, Lukas Malcher, Bernhard Rumpe

+8hTermination Analysis for the $\pi$-Calculus by Reduction to Sequential Program Termination

Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada

+8hArtifact and Reference Models for Generative AI Frameworks and Build Systems

Abdallah Atouani, Jörg Christian Kirchhof, Evgeny Kusmenko, Bernhard Rumpe

14:40

+8hQ&A and discussion

+8hDiscussion, Questions and Answers

15:00

15:20

15:40

-8hAutomated Verification of the Parallel Bellman--Ford Algorithm

Mohsen Safari, Wytse Oortwijn, Marieke Huisman

-8hLeveraging Relational Concept Analysis for Automated Feature Location in Software Product Lines

Nicolas Hlad, Bérénice Lemoine, Marianne Huchard, Abdelhak Seriai

-8hBackward Symbolic Execution with Loop Folding

Marek Chalupa, Jan Strejcek

-8hFIDDLR: Streamlining Reuse with Concern-Specific Modelling Languages

Maximilian Schiedermeier, Jörg Kienzle, Bettina Kemme

16:00

-8hImproving Thread-Modular Abstract Interpretation

Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani

-8hLifted Termination Analysis by Abstract Interpretation and its Applications

Aleksandar S. Dimovski

16:20

-8hSymbolic Automatic Relations and Their Applications to SMT and CHC Solving

Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

-8hDelta-based Verification of Software Product Families

Marco Scaletta, Reiner Hähnle, Dominic Steinhöfel, Richard Bubel

16:40

-8hSession 4B Discussion, Questions and Answers

-8hDiscussion, Questions and Answers

17:00

A Separation Logic for Probabilistic Independence

Type-safe generation of modules in applicative and generative styles

Yuhi Sato, Yukiyoshi Kameyama

HACCLE: Metaprogramming for Secure Multi-Party Computation

Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Nouraldin Jaber, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoit Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni

17:20

Multi-Stage Programming with Generative and Analytical Macros

Nicolas Stucki, Jonathan Immanuel Brachthäuser, Martin Odersky

VirtualGPCE Best Paper Award

17:40

Metaprogramming with Combinators

Mahshid Shahmohammadian, Geoffrey Mainland

18:00

Discussion, Questions and Answers

18:20

18:40

A Typed Programmatic Interface to Contracts on the Blockchain

Thi Thu Ha Doan, Peter Thiemann

Compositional Verification of Smart Contracts Through Communication Abstraction

Scott Wesley, Maria Christakis, Arie Gurfinkel, Jorge A. Navas, Richard Trefler, Valentin Wüstholz

Fast Incremental PEG Parsing

Zachary Yedidia, Stephen Chong

19:00

Adaptable Traces for Program Explanations

Divya Bajaj, Martin Erwig, Danila Fedorin, Kai Gay

Selectively-Amortized Resource Bounding

Tianhan Lu, Bor-Yuh Evan Chang, Ashutosh Trivedi

Faster Reachability Analysis for LR(1) Parsers

Frédéric Bour, François Pottier

19:20

Latent Effects for Reusable Language Components

Birthe van den Berg, Casper Bach Poulsen, Tom Schrijvers, Nicolas Wu

Thread-modular Analysis of Release-Acquire Concurrency

Divyanjali Sharma, Subodh Sharma

Automatic Grammar Repair

Moeketsi Raselimo, Bernd Fischer

The Choice Construct in the Soufflé Language

Xiaowen Hu, Joshua Karp, David Zhao, Abdul Zreika, Xi Wu, Bernhard Scholz

Session 2B Discussion, Questions and Answers

Vision: Bias in Systematic Grammar-Based Test Suite Construction Algorithms

Christoff Rossouw, Bernd Fischer

19:40

Compiling pattern matching to in-place modifications

Q&A and discussion

Discussion, Questions and Answers

20:00

20:20

20:40

21:00

21:20

21:40

Preprocessing of Alternating Automata for Language Emptiness Testing

Pavol Vargovčík, Lukáš Holík

A DSL for Explanatory Decision Making

Martin Erwig, Prashant Kumar

22:00

Proving LTL Properties of Bitvector Programs and Decompiled Binaries

Cyrus Liu, Chengbin Pang, Daniel Dietsch, Eric Koskinen, Ton Chanh Le, Georgios Portokalidis, Jun Xu

SEALS: A framework for building Self-Adaptive Virtual Machines

Gwendal Jouneaux, Olivier Barais, Benoit Combemale, Gunter Mussbacher

22:20

Solving Not-Substring with Flat Abstraction

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, Di-De Yen

Understanding and Improving Model-Driven IoT Systems Through Accompanying Digital Twins

Jörg Christian Kirchhof, Lukas Malcher, Bernhard Rumpe

Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program Termination

Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada

Artifact and Reference Models for Generative AI Frameworks and Build Systems

Abdallah Atouani, Jörg Christian Kirchhof, Evgeny Kusmenko, Bernhard Rumpe

22:40

Q&A and discussion

Discussion, Questions and Answers

23:00

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

Tue 19 Oct

7:20

Hedy: Creating a gradual programming language

Felienne Hermans, Federico Tomassetti

7:40

Fast and Efficient Bit-Level Precision Tuning

Assalé Adjé, Dorra Ben Khalifa, Matthieu Martel

Chair's Welcome and Most Notable Paper Award

Union and Intersection Contracts Are Hard, Actually

Teodoro Freund, Yann Hamdaoui, Arnaud Spiwack

Research PaperVirtual

Reduced Products of Abstract Domains for Fairness Certification of Neural Networks

Denis Mazzucato, Caterina Urban

8:00

Static analysis of ReLU neural networks with tropical polyhedra

Eric Goubault, Sebastien Palumby, Sylvie Putot, Louis Rustenholz, Sriram Sankaranarayanan

Runtime and Compiler Support for HAMTs

Sona Torosyan, Jon Zeppieri, Matthew Flatt

Research PaperVirtual

8:20

Toward Neural-Network-Guided Program Synthesis and Verification

Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno

8:40

Session 4C Discussion, Questions and Answers

9:00

The F# view on the Static / Dynamic divide

Don Syme, Nicholas Matsakis

+8hHow to Navigate SPLASH

Elisa Baniassad

9:20

+8hA Tour through the Program

9:40

+8hMentoring Sessions

10:00

10:20

Invited Speaker

10:40

Pointer Analysis of Bytecode Programs for Effective Formal Verification of Smart Contracts

Invited TalkVirtual

A Retrospective on the Design of the Swift Programming Language

Dave Abrahams, Roman Elizarov, Denys Shabalin

+8hPL/SE Career Panel

Joe Gibbs Politz, Brittany Nkounkou, Youyou Cong, Caroline Lemieux, Andrew Craik, Marek Prochazka

11:00

11:20

11:40

12:00

12:20

12:40

13:00

13:20

13:40

+8hAutomatic Synthesis of Data-Flow Analyzers

Xuezheng Xu, Xudong Wang, Jingling Xue

A Brief History of the API, Revisited

Josh Bloch, Doug Lea

+8hAnalyzing Permission Transfer Channels for Dynamically Typed Languages

Théo Rogliano, Guillermo Polito, Luc Fabresse, Stéphane Ducasse

Research PaperVirtual

14:00

+8hDisjunctive Interval Analysis

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sondergaard, Peter J. Stuckey

+8hOn Design and Use of First-Class Environments in R

Aviral Goel, Jan Vitek

Research PaperVirtual

14:20

+8hHash Consed Points-To Sets

Mohamad Barbar, Yulei Sui

+8hSelective Context-Sensitivity for k-CFA with CFL-Reachability

Jingbo Lu, Dongjie He, Jingling Xue

14:40

+8hCompGen: Generation of Fast JIT Compilers in a Multi-language VM

Florian Latifi, David Leopoldseder, Christian Wimmer, Hanspeter Mössenböck

Research PaperVirtual

+8hSession 3C Discussion, Questions and Answers

15:00

15:20

15:40

-8hFast and Efficient Bit-Level Precision Tuning

Assalé Adjé, Dorra Ben Khalifa, Matthieu Martel

Fragmentation of Machine Architecture

Sean Parent, Mario Wolczko

-8hChair's Welcome and Most Notable Paper Award

-8hUnion and Intersection Contracts Are Hard, Actually

Teodoro Freund, Yann Hamdaoui, Arnaud Spiwack

Research PaperVirtual

-8hReduced Products of Abstract Domains for Fairness Certification of Neural Networks

Denis Mazzucato, Caterina Urban

16:00

-8hStatic analysis of ReLU neural networks with tropical polyhedra

Eric Goubault, Sebastien Palumby, Sylvie Putot, Louis Rustenholz, Sriram Sankaranarayanan

-8hRuntime and Compiler Support for HAMTs

Sona Torosyan, Jon Zeppieri, Matthew Flatt

Research PaperVirtual

16:20

-8hToward Neural-Network-Guided Program Synthesis and Verification

Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno

16:40

-8hSession 4C Discussion, Questions and Answers

17:00

How to Navigate SPLASH

Elisa Baniassad

17:20

A Tour through the Program

17:40

Mentoring Sessions

18:00

18:20

Invited Speaker

Ashley Williams

18:40

PL/SE Career Panel

Joe Gibbs Politz, Brittany Nkounkou, Youyou Cong, Caroline Lemieux, Andrew Craik, Marek Prochazka

19:00

19:20

19:40

20:00

20:20

20:40

21:00

21:20

21:40

Automatic Synthesis of Data-Flow Analyzers

Xuezheng Xu, Xudong Wang, Jingling Xue

Analyzing Permission Transfer Channels for Dynamically Typed Languages

Théo Rogliano, Guillermo Polito, Luc Fabresse, Stéphane Ducasse

Research PaperVirtual

22:00

Disjunctive Interval Analysis

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sondergaard, Peter J. Stuckey

On Design and Use of First-Class Environments in R

Aviral Goel, Jan Vitek

Research PaperVirtual

22:20

Hash Consed Points-To Sets

Mohamad Barbar, Yulei Sui

Selective Context-Sensitivity for k-CFA with CFL-Reachability

Jingbo Lu, Dongjie He, Jingling Xue

22:40

CompGen: Generation of Fast JIT Compilers in a Multi-language VM

Florian Latifi, David Leopoldseder, Christian Wimmer, Hanspeter Mössenböck

Research PaperVirtual

Session 3C Discussion, Questions and Answers

23:00

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

Wed 20 Oct

7:40

The Semantics of Shared Memory in Intel CPU/FPGA Systems

Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, John Wickerson

A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed Programming

Malte Viering, Raymond Hu, Patrick Eugster, Lukasz Ziarek

Making Pointer Analysis More Precise by Unleashing the Power of Selective Context Sensitivity

Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, Yannis Smaragdakis

SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency

Pengbo Yan, Toby Murray

Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems

Wolf Honore, Jieung Kim, Ji-Yong Shin, Zhong Shao

Compacting Points-To Sets through Object Clustering

Mohamad Barbar, Yulei Sui

8:00

The Reads-From Equivalence for the TSO and PSO Memory Models

Truc Lam Bui, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, Viktor Toman

Automatic Migration from Synchronous to Asynchronous JavaScript APIs

Satyajit Gokhale, Alexi Turcotte, Frank Tip

Program Analysis via Efficient Symbolic Abstraction

Peisen Yao, Qingkai Shi, Heqing Huang, Charles Zhang

8:20

Making Weak Memory Models Fair

Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis

Distinguished Paper

QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems

Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, Roopsha Samanta

JavaDL: Automatically Incrementalizing Java Bug Pattern Detection

Alexandru Dura, Christoph Reichenbach, Emma Söderberg

8:40

Discussion, Questions and Answers

Discussion, Questions and Answers

Discussion, Questions and Answers

9:00

Overlapping Events:

SPLASH Conference at Chicago Starts Now

+8h09:00 - 09:20

Opening Session

9:20

+8hExascale and then what?: HPC and AI for Scientific Discovery

9:40

10:00

10:20

Overlapping Events:

+8h10:20 - 10:50

SkyQuery: An Aerial Drone Video Sensing Platform

VirtualOnward! Papers

+8h10:20 - 10:50

Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom

VirtualOnward! Papers

+8h10:20 - 10:50

Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems

+8h10:20 - 10:50

The Semantics of Shared Memory in Intel CPU/FPGA Systems

+8h10:20 - 10:50

Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs

In-Person and VirtualOOPSLA

+8h10:20 - 10:50

Towards Self-Adaptable Languages

VirtualOnward! Papers

Invited Speaker

10:40

+8hCompiling with Continuations, Correctly

Zoe Paraskevopoulou, Anvay Grover

+8hFully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic Bugs

Ting Su, Yichen Yan, Jue Wang, Jingling Sun, Yiheng Xiong, Geguang Pu, Ke Wang, Zhendong Su

+8hOnward! Welcome

11:00

+8hSynbit: Synthesizing Bidirectional Programs using Unidirectional Sketches

Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

+8hPermchecker: A Toolchain for Debugging Memory Managers with Typestate

Karl Cronburg, Sam Guyer

+8hNatural Language-Guided Programming

Geert Heyman, Rafael Huysegems, Pascal Justen, Tom Van Cutsem

11:20

+8hReachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs

Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, Tiark Rompf

+8hGenerative Type-Aware Mutation for Testing SMT Solvers

Jiwon Park, Dominik Winterer, Chengyu Zhang, Zhendong Su

+8hTowards Self-Adaptable Languages

Gwendal Jouneaux, Olivier Barais, Benoit Combemale, Gunter Mussbacher

+8hEfficient Compilation of Algebraic Effect Handlers

Georgios Karachalias, Filip Koprivec, Matija Pretnar, Tom Schrijvers

+8hProgramming and Execution Models for Parallel Bounded Exhaustive Testing

Nader Al Awar, Kush Jain, Chris Rossbach, Milos Gligoric

+8hProgramming with Neural Surrogates of Programs

Alex Renda, Yi Ding, Michael Carbin

11:40

+8hDiscussion, Questions and Answers

+8hDiscussion, Questions and Answers

+8hDiscussion, Questions and Answers

12:00

Faculty Mentoring Roundtable

12:20

12:40

13:00

13:20

13:40

+8hTranslating C to Safer Rust

Mehmet Emre, Ryan Schroeder, Kyle Dewey, Ben Hardekopf

+8hSpecSafe: Detecting Cache Side Channels in a Speculative World

Robert Brotzman-Smith, Danfeng Zhang, Mahmut Taylan Kandemir, Gang (Gary) Tan

+8hKotlin Coroutines: Design and Implementation

Roman Elizarov, Mikhail Belyaev, Marat Akhin, Ilmir Usmanov

14:00

+8hModular Specification and Verification of Closures in Rust

Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, Alexander J. Summers

+8hInterpretable Noninterference Measurement and Its Application to Processor Designs

Ziqiao Zhou, Michael K. Reiter

+8hDala: A Simple Capability-Based Dynamic Language Design for Data Race-Freedom

Kiko Fernandez-Reyes, Isaac Oscar Gariano, James Noble, Erin Greenwood-Thessman, Michael Homer, Tobias Wrigstad

14:20

+8hSafer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust

Natalie Popescu, Ziyang Xu, Sotiris Apostolakis, David I. August, Amit Levy

+8hReconciling Optimization with Secure Compilation

Son Tuan Vu, Albert Cohen, Arnaud de Grandmaison, Christophe Guillon, Karine Heydemann

+8hMotivating Complexity Understanding by Profiling Energy Usage

Joshua B. Gross, Daniel Jacoby, Kevin Coogan, Aaron Helman

+8hDiscussion, Questions and Answers

+8hNot So Fast: Understanding and Mitigating Negative Impacts of Compiler Optimizations on Code Reuse Gadget Sets

Michael D. Brown, Matthew Pruett, Robert Bigelow, Girish Mururu, Santosh Pande

+8hSkyQuery: An Aerial Drone Video Sensing Platform

Favyen Bastani, Songtao He, Ziwen Jiang, Osbert Bastani, Sam Madden

14:40

+8hDiscussion, Questions and Answers

+8hDiscussion, Questions and Answers

15:00

15:20

15:40

-8hThe Semantics of Shared Memory in Intel CPU/FPGA Systems

Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, John Wickerson

-8hA Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed Programming

Malte Viering, Raymond Hu, Patrick Eugster, Lukasz Ziarek

-8hMaking Pointer Analysis More Precise by Unleashing the Power of Selective Context Sensitivity

Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, Yannis Smaragdakis

-8hSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency

Pengbo Yan, Toby Murray

-8hMuch ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems

Wolf Honore, Jieung Kim, Ji-Yong Shin, Zhong Shao

-8hCompacting Points-To Sets through Object Clustering

Mohamad Barbar, Yulei Sui

16:00

-8hThe Reads-From Equivalence for the TSO and PSO Memory Models

Truc Lam Bui, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, Viktor Toman

-8hAutomatic Migration from Synchronous to Asynchronous JavaScript APIs

Satyajit Gokhale, Alexi Turcotte, Frank Tip

-8hProgram Analysis via Efficient Symbolic Abstraction

Peisen Yao, Qingkai Shi, Heqing Huang, Charles Zhang

16:20

-8hMaking Weak Memory Models Fair

Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis

Distinguished Paper

-8hQuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems

Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, Roopsha Samanta

-8hJavaDL: Automatically Incrementalizing Java Bug Pattern Detection

Alexandru Dura, Christoph Reichenbach, Emma Söderberg

16:40

-8hDiscussion, Questions and Answers

-8hDiscussion, Questions and Answers

-8hDiscussion, Questions and Answers

17:00

Opening Session

17:20

Exascale and then what?: HPC and AI for Scientific Discovery

17:40

18:00

18:20

Overlapping Events:

SkyQuery: An Aerial Drone Video Sensing Platform

VirtualOnward! Papers

The Semantics of Shared Memory in Intel CPU/FPGA Systems

Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom

VirtualOnward! Papers

Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs

In-Person and VirtualOOPSLA

Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems

Towards Self-Adaptable Languages

VirtualOnward! Papers

Invited Speaker

18:40

Compiling with Continuations, Correctly

Zoe Paraskevopoulou, Anvay Grover

Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic Bugs

Ting Su, Yichen Yan, Jue Wang, Jingling Sun, Yiheng Xiong, Geguang Pu, Ke Wang, Zhendong Su

Onward! Welcome

19:00

Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches

Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

Permchecker: A Toolchain for Debugging Memory Managers with Typestate

Karl Cronburg, Sam Guyer

Natural Language-Guided Programming

Geert Heyman, Rafael Huysegems, Pascal Justen, Tom Van Cutsem

19:20

Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs

Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, Tiark Rompf

Generative Type-Aware Mutation for Testing SMT Solvers

Jiwon Park, Dominik Winterer, Chengyu Zhang, Zhendong Su

Towards Self-Adaptable Languages

Gwendal Jouneaux, Olivier Barais, Benoit Combemale, Gunter Mussbacher

Efficient Compilation of Algebraic Effect Handlers

Georgios Karachalias, Filip Koprivec, Matija Pretnar, Tom Schrijvers

Programming and Execution Models for Parallel Bounded Exhaustive Testing

Nader Al Awar, Kush Jain, Chris Rossbach, Milos Gligoric

Programming with Neural Surrogates of Programs

Alex Renda, Yi Ding, Michael Carbin

19:40

Discussion, Questions and Answers

Discussion, Questions and Answers

Discussion, Questions and Answers

20:00

20:20

20:40

21:00

21:20

21:40

Translating C to Safer Rust

Mehmet Emre, Ryan Schroeder, Kyle Dewey, Ben Hardekopf

SpecSafe: Detecting Cache Side Channels in a Speculative World

Robert Brotzman-Smith, Danfeng Zhang, Mahmut Taylan Kandemir, Gang (Gary) Tan

Kotlin Coroutines: Design and Implementation

Roman Elizarov, Mikhail Belyaev, Marat Akhin, Ilmir Usmanov

22:00

Modular Specification and Verification of Closures in Rust

Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, Alexander J. Summers

Interpretable Noninterference Measurement and Its Application to Processor Designs

Ziqiao Zhou, Michael K. Reiter

Dala: A Simple Capability-Based Dynamic Language Design for Data Race-Freedom

Kiko Fernandez-Reyes, Isaac Oscar Gariano, James Noble, Erin Greenwood-Thessman, Michael Homer, Tobias Wrigstad

22:20

Safer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust

Natalie Popescu, Ziyang Xu, Sotiris Apostolakis, David I. August, Amit Levy

Reconciling Optimization with Secure Compilation

Son Tuan Vu, Albert Cohen, Arnaud de Grandmaison, Christophe Guillon, Karine Heydemann

Motivating Complexity Understanding by Profiling Energy Usage

Joshua B. Gross, Daniel Jacoby, Kevin Coogan, Aaron Helman

Discussion, Questions and Answers

Not So Fast: Understanding and Mitigating Negative Impacts of Compiler Optimizations on Code Reuse Gadget Sets

Michael D. Brown, Matthew Pruett, Robert Bigelow, Girish Mururu, Santosh Pande

SkyQuery: An Aerial Drone Video Sensing Platform

Favyen Bastani, Songtao He, Ziwen Jiang, Osbert Bastani, Sam Madden

22:40

Discussion, Questions and Answers

Discussion, Questions and Answers

23:00

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

Thu 21 Oct

7:40

Well-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers

Stefanos Chaliasos, Thodoris Sotiropoulos, Georgios-Petros Drosos, Charalambos Ioannis Mitropoulos, Dimitris Mitropoulos, Diomidis Spinellis

Rich Specifications for Ethereum Smart Contract Verification

Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, Alexander J. Summers

Programming as Architecture, Design, and Urban Planning

How Statically-Typed Functional Programmers Write Code

Justin Lubin, Sarah E. Chasins

Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts

Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Konstantinos Triantafyllou, Ilias Tsatiris

8:00

What We Eval in the Shadows: A Large-Scale Study of Eval in R Programs

Aviral Goel, Pierre Donat-Bouillud, Filip Křikava, Christoph Kirsch, Jan Vitek

ECROs: Building Global Scale Systems from Sequential Code

Kevin De Porre, Carla Ferreira, Nuno Preguica, Elisa Gonzalez Boix

8:20

Angelic and Demonic Visitation: School Memories

Discussion, Questions and Answers

Durable Functions: Semantics for Stateful Serverless

Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, Christopher S. Meiklejohn

8:40

Discussion, Questions and Answers

9:00

9:20

+8hIntegrated Scientific Modeling and Lab Automation

9:40

10:00

10:20

Overlapping Events:

+8h10:20 - 10:50

Coarsening Optimization for Differentiable Programming

+8h10:20 - 10:50

Statically Bounded-Memory Delayed Sampling for Probabilistic Streams

In-Person and VirtualOOPSLA

+8h10:20 - 10:50

Compilation of Sparse Array Programming Models

In-Person and VirtualOOPSLA

+8h10:20 - 10:50

Study of the Subtyping Machine of Nominal Subtyping with Variance

VirtualDemoOOPSLA

10:40

+8hDynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations

Didier Ishimwe, KimHao Nguyen, ThanhVu Nguyen

+8hGradually Structured Data

Stefan Malewski, Michael Greenberg, Éric Tanter

+8hFuture of Conferences

Stephen Kell, Jonathan Aldrich, Shriram Krishnamurthi, David Grove, Gorel Hedin, Amal Ahmed, Manu Sridharan, Yannis Smaragdakis, Eelco Visser, Sophia Drossopoulou, Tony Hosking, Alex Potanin

VirtualIn-Person

11:00

+8hStatic Detection of Silent Misconfigurations with Deep Interaction Analysis

Jialu Zhang, Ruzica Piskac, Ennan Zhai, Tianyin Xu

+8hSolver-Based Gradual Type Migration

Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, Arjun Guha

11:20

+8hData-Driven Abductive Inference of Library Specifications

Zhe Zhou, Robert Dickerson, Benjamin Delaware, Suresh Jagannathan

+8hSimTyper: Sound Type Inference for Ruby using Type Equality Prediction

Milod Kazerounian, Jeffrey S. Foster, Bonan Min

+8hSynthesizing Contracts Correct Modulo a Test Generator

Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan, Tao Xie

+8hPromises Are Made to Be Broken: Migrating R to Strict Semantics

Aviral Goel, Jan Ječmen, Sebastián Krynski, Olivier Flückiger, Jan Vitek

11:40

+8hDiscussion, Questions and Answers

+8hDiscussion, Questions and Answers

12:00

Faculty Mentoring Roundtable

12:20

12:40

13:00

13:20

13:40

+8hStudy of the Subtyping Machine of Nominal Subtyping with Variance

Distinguished Paper

+8hGeneralizable Synthesis through Unification

Ruyi Ji, Jingtao Xia, Yingfei Xiong, Zhenjiang Hu

+8hCoarsening Optimization for Differentiable Programming

Xipeng Shen, Guoqiang Zhang, Irene Dea, Samantha Andow, Emilio Arroyo-Fang, Neal Gafter, Johann George, Melissa Grueter, Erik Meijer, Olin Grigsby Shivers, Steffi Stumpos, Alanna Tempest, Christy Warden, Shannon Yang

14:00

+8hLabel Dependent Lambda Calculus and Gradual Typing

Weili Fu, Fabian Krause, Peter Thiemann

+8hGauss: Program Synthesis by Reasoning over Graphs

Rohan Bavishi, Caroline Lemieux, Koushik Sen, Ion Stoica

+8hEfficient Automatic Scheduling of Imaging and Vision Pipelines for the GPU

Luke Anderson, Andrew Adams, Karima Ma, Tzu-Mao Li, Tian Jin, Jonathan Ragan-Kelley

14:20

+8hRelational Nullable Types with Boolean Unification

Magnus Madsen, Jaco van de Pol

+8hAPIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in Libraries

Xiang Gao, Arjun Radhakrishna, Gustavo Soares, Ridwan Salihin Shariffdeen, Sumit Gulwani, Abhik Roychoudhury

+8hStatically Bounded-Memory Delayed Sampling for Probabilistic Streams

Eric Atkinson, Guillaume Baudart, Louis Mandel, Charles Yuan, Michael Carbin

+8hType Stability in Julia: Avoiding Performance Pathologies in JIT Compilation

Artem Pelenitsyn, Julia Belyakova, Benjamin Chung, Ross Tate, Jan Vitek

+8hLooPy: Interactive Program Synthesis with Control Structures

Kasra Ferdowsi, Shraddha Barke, Hila Peleg, Sorin Lerner, Nadia Polikarpova

+8hCompilation of Sparse Array Programming Models

Rawn Henry, Olivia Hsu, Rohan Yadav, Stephen Chou, Kunle Olukotun, Saman Amarasinghe, Fredrik Kjolstad

14:40

+8hDiscussion, Questions and Answers

+8hDiscussion, Questions and Answers

+8hDiscussion, Questions and Answers

15:00

15:20

15:40

-8hWell-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers

Stefanos Chaliasos, Thodoris Sotiropoulos, Georgios-Petros Drosos, Charalambos Ioannis Mitropoulos, Dimitris Mitropoulos, Diomidis Spinellis

-8hRich Specifications for Ethereum Smart Contract Verification

Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, Alexander J. Summers

-8hProgramming as Architecture, Design, and Urban Planning

-8hHow Statically-Typed Functional Programmers Write Code

Justin Lubin, Sarah E. Chasins

-8hSymbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts

Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Konstantinos Triantafyllou, Ilias Tsatiris

16:00

-8hWhat We Eval in the Shadows: A Large-Scale Study of Eval in R Programs

Aviral Goel, Pierre Donat-Bouillud, Filip Křikava, Christoph Kirsch, Jan Vitek

-8hECROs: Building Global Scale Systems from Sequential Code

Kevin De Porre, Carla Ferreira, Nuno Preguica, Elisa Gonzalez Boix

16:20

-8hAngelic and Demonic Visitation: School Memories

-8hDiscussion, Questions and Answers

-8hDurable Functions: Semantics for Stateful Serverless

Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, Christopher S. Meiklejohn

16:40

-8hDiscussion, Questions and Answers

17:00

17:20

Integrated Scientific Modeling and Lab Automation

17:40

18:00

18:20

Overlapping Events:

Study of the Subtyping Machine of Nominal Subtyping with Variance

VirtualDemoOOPSLA

Statically Bounded-Memory Delayed Sampling for Probabilistic Streams

In-Person and VirtualOOPSLA

Compilation of Sparse Array Programming Models

In-Person and VirtualOOPSLA

Coarsening Optimization for Differentiable Programming

18:40

Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations

Didier Ishimwe, KimHao Nguyen, ThanhVu Nguyen

Gradually Structured Data

Stefan Malewski, Michael Greenberg, Éric Tanter

Future of Conferences

Stephen Kell, Jonathan Aldrich, Shriram Krishnamurthi, David Grove, Gorel Hedin, Amal Ahmed, Manu Sridharan, Yannis Smaragdakis, Eelco Visser, Sophia Drossopoulou, Tony Hosking, Alex Potanin

VirtualIn-Person

19:00

Static Detection of Silent Misconfigurations with Deep Interaction Analysis

Jialu Zhang, Ruzica Piskac, Ennan Zhai, Tianyin Xu

Solver-Based Gradual Type Migration

Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, Arjun Guha

19:20

Data-Driven Abductive Inference of Library Specifications

Zhe Zhou, Robert Dickerson, Benjamin Delaware, Suresh Jagannathan

SimTyper: Sound Type Inference for Ruby using Type Equality Prediction

Milod Kazerounian, Jeffrey S. Foster, Bonan Min

Synthesizing Contracts Correct Modulo a Test Generator

Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan, Tao Xie

Promises Are Made to Be Broken: Migrating R to Strict Semantics

Aviral Goel, Jan Ječmen, Sebastián Krynski, Olivier Flückiger, Jan Vitek

19:40

Discussion, Questions and Answers

Discussion, Questions and Answers

20:00

20:20

20:40

21:00

21:20

21:40

Study of the Subtyping Machine of Nominal Subtyping with Variance

Distinguished Paper

Generalizable Synthesis through Unification

Ruyi Ji, Jingtao Xia, Yingfei Xiong, Zhenjiang Hu

Coarsening Optimization for Differentiable Programming

Xipeng Shen, Guoqiang Zhang, Irene Dea, Samantha Andow, Emilio Arroyo-Fang, Neal Gafter, Johann George, Melissa Grueter, Erik Meijer, Olin Grigsby Shivers, Steffi Stumpos, Alanna Tempest, Christy Warden, Shannon Yang

22:00

Label Dependent Lambda Calculus and Gradual Typing

Weili Fu, Fabian Krause, Peter Thiemann

Gauss: Program Synthesis by Reasoning over Graphs

Rohan Bavishi, Caroline Lemieux, Koushik Sen, Ion Stoica

Efficient Automatic Scheduling of Imaging and Vision Pipelines for the GPU

Luke Anderson, Andrew Adams, Karima Ma, Tzu-Mao Li, Tian Jin, Jonathan Ragan-Kelley

22:20

Relational Nullable Types with Boolean Unification

Magnus Madsen, Jaco van de Pol

APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in Libraries

Xiang Gao, Arjun Radhakrishna, Gustavo Soares, Ridwan Salihin Shariffdeen, Sumit Gulwani, Abhik Roychoudhury

Statically Bounded-Memory Delayed Sampling for Probabilistic Streams

Eric Atkinson, Guillaume Baudart, Louis Mandel, Charles Yuan, Michael Carbin

Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation

Artem Pelenitsyn, Julia Belyakova, Benjamin Chung, Ross Tate, Jan Vitek

LooPy: Interactive Program Synthesis with Control Structures

Kasra Ferdowsi, Shraddha Barke, Hila Peleg, Sorin Lerner, Nadia Polikarpova

Compilation of Sparse Array Programming Models

Rawn Henry, Olivia Hsu, Rohan Yadav, Stephen Chou, Kunle Olukotun, Saman Amarasinghe, Fredrik Kjolstad

22:40

Discussion, Questions and Answers

Discussion, Questions and Answers

Discussion, Questions and Answers

23:00

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

Fri 22 Oct

9:00

+8hIntroduction to SPLASH 2022

+8hSPLASH Awards

9:20

+8hDesigning Safe Programmed Molecular Systems

9:40

10:00

10:20

Overlapping Events:

+8h10:20 - 10:50

Formal Verification of High-Level Synthesis

Yann Herklotz, James D. Pollard, Nadesh Ramanathan, John Wickerson

VirtualDemoOOPSLA

+8h10:20 - 10:50

Scalability and Precision by Combining Expressive Type Systems and Deductive Verification

Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, Werner Dietl

VirtualDemoOOPSLA

10:40

+8hRewrite Rule Inference Using Equality Saturation

Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock

Distinguished Paper

+8hCopy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level Languages and Bytecode

Haoran Xu, Fredrik Kjolstad

Distinguished Paper

+8hUDF to SQL Translation through Compositional Lazy Inductive Synthesis

Guoqiang Zhang, Yuanchao Xu, Xipeng Shen, Işıl Dillig

11:00

+8hSemantic Programming by Example with Pre-trained Models

Gust Verbruggen, Vu Le, Sumit Gulwani

+8hVESPA: Static Profiling for Binary Optimization

Angelica Moreira, Guilherme Ottoni, Fernando Magno Quintão Pereira

+8hLXM: Better Splittable Pseudorandom Number Generators (and Almost as Fast)

Guy L. Steele Jr., Sebastiano Vigna

11:20

+8hOne Down, 699 to Go: or, Synthesising Compositional Desugarings

Sándor Bartha, James Cheney, Vaishak Belle

+8hA Derivative-Based Parser Generator for Visibly Pushdown Grammars

Xiaodong Jia, Ashish Kumar, Gang (Gary) Tan

+8hFPL: Fast Presburger Arithmetic through Transprecision

Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, Tobias Grosser

Distinguished Paper

+8hMulti-modal Program Inference: A Marriage of Pre-trained Language Models and Component-Based Synthesis

Kia Rahmani, Mohammad Raza, Sumit Gulwani, Vu Le, Daniel Morris, Arjun Radhakrishna, Gustavo Soares, Ashish Tiwari

+8hDiscussion, Questions and Answers

+8hVerifying Concurrent Multicopy Search Structures

Nisarg Patel, Siddharth Krishna, Dennis Shasha, Thomas Wies

11:40

+8hDiscussion, Questions and Answers

+8hDiscussion, Questions and Answers

12:00

12:20

12:40

13:00

13:20

13:40

+8hScalability and Precision by Combining Expressive Type Systems and Deductive Verification

Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, Werner Dietl

+8hMonkeyDB: Effectively Testing Correctness under Weak Isolation Levels

Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, Akash Lal

Distinguished Paper

+8hLet a Thousand Flowers Bloom: On the Uses of Diversity in Software Testing

14:00

+8hA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs

Paul He, Edwin Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic

+8hFormal Verification of High-Level Synthesis

Yann Herklotz, James D. Pollard, Nadesh Ramanathan, John Wickerson

14:20

+8hTransitioning from Structural to Nominal Code with Efficient Gradual Typing

Fabian Muehlboeck, Ross Tate

+8hSpecifying and Testing GPU Workgroup Progress Models

Tyler Sorensen, Lucas Fernan Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, Alastair F. Donaldson

+8hThe Kingdoms of Objects and Values

Friedrich Steimann

+8hDiscussion, Questions and Answers

+8hDiscussion, Questions and Answers

14:40

15:00

Ice Cream Social

15:20

15:40

16:00

16:20

16:40

17:00

Introduction to SPLASH 2022

SPLASH Awards

17:20

Designing Safe Programmed Molecular Systems

17:40

18:00

18:20

Overlapping Events:

Scalability and Precision by Combining Expressive Type Systems and Deductive Verification

Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, Werner Dietl

VirtualDemoOOPSLA

Formal Verification of High-Level Synthesis

Yann Herklotz, James D. Pollard, Nadesh Ramanathan, John Wickerson

VirtualDemoOOPSLA

18:40

Rewrite Rule Inference Using Equality Saturation

Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock

Distinguished Paper

Copy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level Languages and Bytecode

Haoran Xu, Fredrik Kjolstad

Distinguished Paper

UDF to SQL Translation through Compositional Lazy Inductive Synthesis

Guoqiang Zhang, Yuanchao Xu, Xipeng Shen, Işıl Dillig

19:00

Semantic Programming by Example with Pre-trained Models

Gust Verbruggen, Vu Le, Sumit Gulwani

VESPA: Static Profiling for Binary Optimization

Angelica Moreira, Guilherme Ottoni, Fernando Magno Quintão Pereira

LXM: Better Splittable Pseudorandom Number Generators (and Almost as Fast)

Guy L. Steele Jr., Sebastiano Vigna

19:20

One Down, 699 to Go: or, Synthesising Compositional Desugarings

Sándor Bartha, James Cheney, Vaishak Belle

A Derivative-Based Parser Generator for Visibly Pushdown Grammars

Xiaodong Jia, Ashish Kumar, Gang (Gary) Tan

FPL: Fast Presburger Arithmetic through Transprecision

Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, Tobias Grosser

Distinguished Paper

Multi-modal Program Inference: A Marriage of Pre-trained Language Models and Component-Based Synthesis

Kia Rahmani, Mohammad Raza, Sumit Gulwani, Vu Le, Daniel Morris, Arjun Radhakrishna, Gustavo Soares, Ashish Tiwari

Discussion, Questions and Answers

Verifying Concurrent Multicopy Search Structures

Nisarg Patel, Siddharth Krishna, Dennis Shasha, Thomas Wies

19:40

Discussion, Questions and Answers

Discussion, Questions and Answers

20:00

20:20

20:40

21:00

21:20

21:40

Scalability and Precision by Combining Expressive Type Systems and Deductive Verification

Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, Werner Dietl

MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels

Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, Akash Lal

Distinguished Paper

Let a Thousand Flowers Bloom: On the Uses of Diversity in Software Testing

22:00

A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs

Paul He, Edwin Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic

Formal Verification of High-Level Synthesis

Yann Herklotz, James D. Pollard, Nadesh Ramanathan, John Wickerson

22:20

Transitioning from Structural to Nominal Code with Efficient Gradual Typing

Fabian Muehlboeck, Ross Tate

Specifying and Testing GPU Workgroup Progress Models

Tyler Sorensen, Lucas Fernan Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, Alastair F. Donaldson

The Kingdoms of Objects and Values

Friedrich Steimann

Discussion, Questions and Answers

Discussion, Questions and Answers

22:40

23:00