PPDP 2023
Sun 22 - Mon 23 October 2023 Cascais, Portugal
co-located with SPLASH 2023
VenueHotel Cascais Miragem
Room nameRoom I
Floor0
Capacity392
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 22 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Session 1SAS at Room I
Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL
09:00
5m
Opening
SAS
Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, José Morales IMDEA Software Institute
Pre-print
09:05
60m
Keynote
Goal-Directed Abstract Interpretation and Event-Driven FrameworksKeynote
SAS
I: Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon
Pre-print
10:05
30m
Talk
A Product of Shape and Sequence Abstractions (Radhia Cousot Young Researcher Best Paper Award)
SAS
Josselin Giet Ecole Normale Supérieure, Félix Ridoux Univ Rennes / IMDEA Software Institute, Xavier Rival Inria; ENS; CNRS; PSL University
Pre-print
11:00 - 12:30
Domain precisionSAS at Room I
Chair(s): Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon
11:00
30m
Talk
How fitting is your abstract domain?
SAS
Roberto Giacobazzi University of Arizona, Isabella Mastroeni University of Verona, Italy, Elia Perantoni University of Verona
Pre-print
11:30
30m
Talk
Domain Precision in Galois Connection-less Abstract Interpretation
SAS
Isabella Mastroeni University of Verona, Italy, Michele Pasqua University of Verona
Pre-print
12:00
30m
Talk
A Formal Framework to Measure the Incompleteness of Abstract Interpretations
SAS
Marco Campion INRIA & École Normale Supérieure | Université PSL, Caterina Urban Inria & École Normale Supérieure | Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona
Pre-print
14:00 - 15:30
Synthesis and applicationsSAS at Room I
Chair(s): Daniel Schoepe Amazon
14:00
30m
Talk
Generalized Program Sketching by Abstract Interpretation and Logical Abduction
SAS
Aleksandar S. Dimovski Mother Teresa University, Skopje
Pre-print File Attached
14:30
30m
Talk
Reverse Template Processing using Abstract Interpretation
SAS
Matthieu Lemerre Université Paris-Saclay - CEA LIST
Pre-print
15:00
30m
Talk
BREWasm: A General Static Binary Rewriting Framework for WebAssemblyRemote
SAS
Shangtong Cao Beijing University of Posts and Telecommunications, Ningyu He Peking University, Yao Guo Peking University, Haoyu Wang Huazhong University of Science and Technology
Pre-print
16:00 - 17:30
Quantum, neuralSAS at Room I
Chair(s): Roberto Giacobazzi University of Arizona
16:00
30m
Talk
Quantum Constant Propagation
SAS
Yanbin Chen TUM School of Computation, Information and Technology, Technical University of Munich, Yannick Stade TUM School of Computation, Information and Technology, Technical University of Munich
Pre-print
16:30
30m
Talk
Boosting Multi-Neuron Convex Relaxation for Neural Network Verification
SAS
Xuezhou Tang ShenZhen University, Ye Zheng Shenzhen University, Jiaxiang Liu Shenzhen University
Pre-print
17:30 - 19:30
MPLR PostersMPLR at Room I

MPLR posters will be presented during the SPLASH poster sessions, Sunday 22 October 5:30PM - 7:30PM and Tuesday 24 October 5:30PM - 7:30PM.

17:30
40m
Talk
CloudJIT: A Just-in-Time FaaS Optimizer (Poster Abstract)
MPLR
Serhii Ivanenko INESC-ID; IST-ULisboa, Rodrigo Bruno INESC-ID - IST-ULisboa, Jovan Stevanovic Oracle Labs, Luís Veiga INESC-ID; IST-ULisboa, Vojin Jovanovic Oracle Labs
DOI
18:10
40m
Talk
Don’t Trust Your Profiler: An Empirical Study on the Precision and Accuracy of Java Profilers (Poster Abstract)
MPLR
Humphrey Burchell University of Kent, Octave Larose University of Kent, Sophie Kaleba University of Kent, Stefan Marr University of Kent
DOI
18:50
40m
Talk
Diagnosing Compiler Performance by Comparing Optimization Decisions (Poster Abstract)
MPLR
Andrej Pečimúth Oracle Labs; Charles University, David Leopoldseder Oracle Labs, Petr Tuma Charles University
DOI
17:30 - 19:30
SPLASH PostersSPLASH Posters at Room I
Chair(s): Xujie Si University of Toronto
17:30
2h
Poster
Sui Move: Modern Blockchain Programming with Objects
SPLASH Posters
Adam Welc Mysten Labs, Sam Blackshear Mysten Labs
17:30
2h
Poster
Safe Combination of Data-centric and Operation-centric Consistency
SPLASH Posters
Mirko Köhler TU Darmstadt, Guido Salvaneschi University of St. Gallen
17:30
2h
Poster
Dynamic Library Compartmentalization
SPLASH Posters
Octave Larose University of Kent
17:30
2h
Poster
Collabs implements collaborative data structures (CRDTs) with OOP principles
SPLASH Posters
Matthew Weidner Carnegie Mellon University
17:30
2h
Poster
Involving Users in Design of a Widely Used Language: A Case of ECMAScript (JavaScript) Standardization
SPLASH Posters
Mikhail Barash University of Bergen, Yulia Startsev Mozilla, Rolf Martin Glomsrud University of Bergen (Norway)
17:30
2h
Poster
A Functional Reactive Programming Language for Wirelessly Connected Shape-Changeable Chiplet-Based Computers
SPLASH Posters
Yusuke Izawa IBM Research - Tokyo, Junichiro Kadomoto The University of Tokyo, Hidetsugu Irie University of Tokyo, Shuichi Sakai University of Tokyo
17:30
2h
Poster
Kind Inference for the FreeST Programming Language
SPLASH Posters
Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Andreia Mordido LASIGE, University of Lisbon, Vasco T. Vasconcelos LASIGE, University of Lisbon
17:30
2h
Poster
Extensible Testing for Infrastructure as Code
SPLASH Posters
David Spielmann University of St. Gallen, Daniel Sokolowski University of St. Gallen, Guido Salvaneschi University of St. Gallen
17:30
2h
Poster
Penrose: Beautiful diagrams from plain text
SPLASH Posters
Sam Estep Carnegie Mellon University
17:30
2h
Poster
JaMaBuild: Mass Building of Java Projects
SPLASH Posters
Matúš Sulír Technical University of Košice, Milan Nosáľ ValeSoft, s.r.o.
17:30
2h
Poster
Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs
SPLASH Posters
Tobias Reinhard KU Leuven, Justus Fasse Université Grenoble-Alpes; KU Leuven, Bart Jacobs KU Leuven
17:30
2h
Poster
Towards Reusable GUI Structures
SPLASH Posters
Knut Anders Stokke University of Bergen, Norway, Mikhail Barash University of Bergen, Jaakko Järvi University of Bergen
17:30
2h
Poster
ReactCOP: Modular and Scalable Web Development with Context-Oriented Programming
SPLASH Posters
David H. Lorenz Open University of Israel, Ofir Shmuel Open University of Israel
DOI Media Attached
17:30
2h
Poster
Generating Domain-Specific Programs for Diagram Authoring with Large Language Models
SPLASH Posters
Rijul Jain Williams College, Wode Ni Columbia University, Joshua Sunshine Carnegie Mellon University

Mon 23 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
Modular arithmetic and numeric analysisSAS at Room I
Chair(s): Daniel Kaestner AbsInt
11:00
30m
Talk
Symbolic transformation of expressions in modular arithmetic
SAS
Jérôme Boillot École Normale Supérieure, PSL University & INRIA, Jerome Feret INRIA Paris
Pre-print
11:30
30m
Talk
Polynomial Analysis of Modular Arithmetic
SAS
Thomas Seed University of Kent, Andy King Kent, Neil Evans AWE, Chris Coppins University of Kent
Pre-print
12:00
30m
Talk
Octagons Revisited - Elegant Proofs and Simplified Algorithms
SAS
Michael Schwarz Technische Universität München, Helmut Seidl Technische Universität München
Pre-print
14:00 - 15:30
Error location and scalingSAS at Room I
Chair(s): Andy King Kent
14:00
30m
Talk
Error Invariants for Fault Localization via Abstract Interpretation
SAS
Aleksandar S. Dimovski Mother Teresa University, Skopje
Pre-print File Attached
14:30
30m
Talk
Error Localization for Sequential Effect Systems
SAS
Colin Gordon Drexel University, Chaewon Yun Drexel University
Link to publication Pre-print
15:00
30m
Talk
Scaling up Roundoff Analysis of Functional Data Structure Programs
SAS
Anastasia Isychev Technical University of Vienna, Eva Darulova Uppsala University
Pre-print
16:00 - 17:30
Session 8SAS at Room I
Chair(s): José Morales IMDEA Software Institute, Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute
16:00
60m
Keynote
Building Trust and Safety in Artificial Intelligence with Abstract InterpretationRemoteKeynote
SAS
I: Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research
Pre-print
17:00
30m
Awards
Radhia Cousot Award and PC report
SAS
C: Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, C: José Morales IMDEA Software Institute

Tue 24 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Cost/precision trade-offs and accelerationSAS at Room I
Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University
09:00
30m
Talk
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
SAS
Florian Frohn RWTH Aachen University, Jürgen Giesl RWTH Aachen University
Pre-print
09:30
30m
Talk
Unconstrained Variable Oracles for Faster Static Analyses
SAS
Vincenzo Arceri University of Parma, Italy, Greta Dolcetti University of Parma - Department of Mathematical, Physical, and Computer Sciences, Enea Zaffanella University of Parma, Italy
Pre-print
10:00
30m
Talk
Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs
SAS
Rosa Abbasi Boroujeni Max Planck Institute for Software Systems, Eva Darulova Uppsala University
Pre-print
11:00 - 12:30
Session 10SAS at Room I
Chair(s): Jerome Feret INRIA Paris
11:00
60m
Keynote
Verifying Infinitely Many Programs at OnceKeynote
SAS
I: Loris D'Antoni University of Wisconsin-Madison
Pre-print
12:00
30m
Talk
Mutual Refinements of Context-Free Language Reachability
SAS
Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
Pre-print
17:30 - 19:30
SPLASH PostersSPLASH Posters at Room I
17:30
8m
Poster
Extensible Testing for Infrastructure as Code
SPLASH Posters
David Spielmann University of St. Gallen, Daniel Sokolowski University of St. Gallen, Guido Salvaneschi University of St. Gallen
17:38
8m
Poster
ReactCOP: Modular and Scalable Web Development with Context-Oriented Programming
SPLASH Posters
David H. Lorenz Open University of Israel, Ofir Shmuel Open University of Israel
DOI Media Attached
17:47
8m
Poster
Involving Users in Design of a Widely Used Language: A Case of ECMAScript (JavaScript) Standardization
SPLASH Posters
Mikhail Barash University of Bergen, Yulia Startsev Mozilla, Rolf Martin Glomsrud University of Bergen (Norway)
17:55
8m
Poster
Kind Inference for the FreeST Programming Language
SPLASH Posters
Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Andreia Mordido LASIGE, University of Lisbon, Vasco T. Vasconcelos LASIGE, University of Lisbon
18:04
8m
Poster
Collabs implements collaborative data structures (CRDTs) with OOP principles
SPLASH Posters
Matthew Weidner Carnegie Mellon University
18:12
8m
Poster
Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs
SPLASH Posters
Tobias Reinhard KU Leuven, Justus Fasse Université Grenoble-Alpes; KU Leuven, Bart Jacobs KU Leuven
18:21
8m
Poster
Dynamic Library Compartmentalization
SPLASH Posters
Octave Larose University of Kent
18:30
8m
Poster
JaMaBuild: Mass Building of Java Projects
SPLASH Posters
Matúš Sulír Technical University of Košice, Milan Nosáľ ValeSoft, s.r.o.
18:38
8m
Poster
Sui Move: Modern Blockchain Programming with Objects
SPLASH Posters
Adam Welc Mysten Labs, Sam Blackshear Mysten Labs
18:47
8m
Poster
Towards Reusable GUI Structures
SPLASH Posters
Knut Anders Stokke University of Bergen, Norway, Mikhail Barash University of Bergen, Jaakko Järvi University of Bergen
18:55
8m
Poster
A Functional Reactive Programming Language for Wirelessly Connected Shape-Changeable Chiplet-Based Computers
SPLASH Posters
Yusuke Izawa IBM Research - Tokyo, Junichiro Kadomoto The University of Tokyo, Hidetsugu Irie University of Tokyo, Shuichi Sakai University of Tokyo
19:04
8m
Poster
Generating Domain-Specific Programs for Diagram Authoring with Large Language Models
SPLASH Posters
Rijul Jain Williams College, Wode Ni Columbia University, Joshua Sunshine Carnegie Mellon University
19:12
8m
Poster
Safe Combination of Data-centric and Operation-centric Consistency
SPLASH Posters
Mirko Köhler TU Darmstadt, Guido Salvaneschi University of St. Gallen
19:21
8m
Poster
Penrose: Beautiful diagrams from plain text
SPLASH Posters
Sam Estep Carnegie Mellon University

Wed 25 Oct

Displayed time zone: Lisbon change

09:00 - 09:30
Opening and WelcomeSPLASH OOPSLA at Room I
Chair(s): Vasco T. Vasconcelos LASIGE, University of Lisbon
  • Welcome to SPLASH
  • OOPSLA Review Committee Board report, including Distinguished OOPSLA 2023 papers
09:00
30m
Other
Opening and Welcome
SPLASH OOPSLA

11:00 - 12:30
AI4SESPLASH OOPSLA at Room I
Chair(s): Guido Salvaneschi University of St. Gallen
11:00
18m
Talk
Grounded Copilot: How Programmers Interact with Code-Generating ModelsDistinguished Paper
SPLASH OOPSLA
Shraddha Barke University of California at San Diego, Michael B. James University of California at San Diego, Nadia Polikarpova University of California at San Diego
DOI
11:18
18m
Talk
Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs
SPLASH OOPSLA
Alex Renda Massachusetts Institute of Technology, Yi Ding Purdue University, Michael Carbin Massachusetts Institute of Technology
DOI Pre-print
11:36
18m
Talk
Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving
SPLASH OOPSLA
Fangke Ye Georgia Institute of Technology, Jisheng Zhao Georgia Institute of Technology, Jun Shirako Georgia Institute of Technology, Vivek Sarkar Georgia Institute of Technology
DOI
11:54
18m
Talk
An Explanation Method for Models of Code
SPLASH OOPSLA
Yu Wang Nanjing University, Ke Wang , Linzhang Wang Nanjing University
DOI
12:12
18m
Talk
Optimization-Aware Compiler-Level Event Profiling
SPLASH OOPSLA
Matteo Basso Università della Svizzera italiana (USI), Switzerland, Aleksandar Prokopec Oracle Labs, Andrea Rosà USI Lugano, Walter Binder USI Lugano
Link to publication DOI
14:00 - 15:30
SE4AISPLASH OOPSLA at Room I
Chair(s): Arjun Guha Northeastern University; Roblox
14:00
18m
Talk
Run-Time Prevention of Software Integration Failures of Machine Learning APIs
SPLASH OOPSLA
Chengcheng Wan East China Normal University, Yuhan Liu University of Chicago, Kuntai Du University of Chicago, Henry Hoffmann University of Chicago, Junchen Jiang University of Chicago, Michael Maire University of Chicago, Shan Lu Microsoft; University of Chicago
DOI
14:18
18m
Talk
Compiling Structured Tensor Algebra
SPLASH OOPSLA
Mahdi Ghorbani University of Edinburgh, Mathieu Huot University of Oxford, Shideh Hashemian University of Edinburgh, Amir Shaikhha University of Edinburgh
DOI
14:36
18m
Talk
Perception Contracts for Safety of ML-Enabled Systems
SPLASH OOPSLA
Angello Astorga University of Illinois at Urbana-Champaign, Chiao Hsieh Kyoto University, P. Madhusudan University of Illinois at Urbana-Champaign, Sayan Mitra University of Illinois at Urbana-Champaign
DOI
14:54
18m
Talk
Languages with Decidable Learning: A Meta-theoremDistinguished Paper
SPLASH OOPSLA
Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
DOI
15:12
18m
Talk
Deep Learning Robustness Verification for Few-Pixel Attacks
SPLASH OOPSLA
Yuval Shapira Technion, Eran Avneri Technion, Dana Drachsler Cohen Technion
DOI
16:00 - 17:30
probabilisticSPLASH OOPSLA at Room I
Chair(s): Chandrakana Nandi Certora
16:00
18m
Talk
A Deductive Verification Infrastructure for Probabilistic Programs
SPLASH OOPSLA
Philipp Schröer RWTH Aachen University, Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU
DOI
16:18
18m
Talk
A Gradual Probabilistic Lambda Calculus
SPLASH OOPSLA
Wenjia Ye University of Hong Kong, Matías Toro University of Chile, Federico Olmedo University of Chile
DOI
16:36
18m
Talk
Lower Bounds for Possibly Divergent Probabilistic Programs
SPLASH OOPSLA
Shenghua Feng Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingshuai Chen Zhejiang University, Han Su Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Naijun Zhan Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
Link to publication DOI Pre-print
16:54
18m
Talk
Exact Recursive Probabilistic Programming
SPLASH OOPSLA
David Chiang University of Notre Dame, Colin McDonald University of Notre Dame, Chung-chieh Shan Indiana University
DOI
17:12
18m
Talk
Solving String Constraints with Lengths by StabilizationDistinguished Paper
SPLASH OOPSLA
Yu-Fang Chen Academia Sinica, David Chocholatý Brno University of Technology, Vojtěch Havlena Brno University of Technology, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Juraj Síč Brno University of Technology
DOI

Thu 26 Oct

Displayed time zone: Lisbon change

09:30 - 10:30
Keynote 2SPLASH OOPSLA at Room I
Chair(s): Mira Mezini TU Darmstadt
09:30
60m
Keynote
Hydroflow: A Compiler Target for Fast, Correct Distributed ProgramsKeynote
SPLASH OOPSLA
11:00 - 12:30
type systems 1SPLASH OOPSLA at Room I
Chair(s): Max S. New University of Michigan
11:00
18m
Talk
Reference Capabilities for Flexible Memory Management
SPLASH OOPSLA
Ellen Arvidsson Uppsala University, Elias Castegren Uppsala University, Sylvan Clebsch Microsoft Azure Research, Sophia Drossopoulou Imperial College London, James Noble Research & Programming, Matthew J. Parkinson Microsoft Azure Research, Tobias Wrigstad Uppsala University
DOI Pre-print
11:18
18m
Talk
A Grounded Conceptual Model for Ownership Types in Rust
SPLASH OOPSLA
Will Crichton Brown University, Gavin Gray ETH Zurich, Shriram Krishnamurthi Brown University
DOI Pre-print
11:36
18m
Talk
Inference of Resource Management Specifications
SPLASH OOPSLA
Narges Shadab University of California at Riverside, Pritam Gharat Microsoft Research, Shrey Tiwari Microsoft Research, Michael D. Ernst University of Washington, Martin Kellogg New Jersey Institute of Technology, Shuvendu K. Lahiri Microsoft Research, Akash Lal Microsoft Research, Manu Sridharan University of California at Riverside
DOI
11:54
18m
Talk
Resource-Aware Soundness for Big-Step Semantics
SPLASH OOPSLA
Riccardo Bianchini University of Genoa, Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa
DOI
12:12
18m
Talk
Verus: Verifying Rust Programs using Linear Ghost Types
SPLASH OOPSLA
Andrea Lattuada VMware Research, Travis Hance Carnegie Mellon University, Chanhee Cho Carnegie Mellon University, Matthias Brun ETH Zurich, Isitha Subasinghe UNSW Sydney, Yi Zhou Carnegie Mellon University, Jon Howell VMware Research, Bryan Parno Carnegie Mellon University, Chris Hawblitzel Microsoft Research
DOI
14:00 - 15:30
type systems 2SPLASH OOPSLA at Room I
Chair(s): Max S. New University of Michigan
14:00
18m
Talk
Greedy Implicit Bounded Quantification
SPLASH OOPSLA
Chen Cui University of Hong Kong, Shengyi Jiang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
14:18
18m
Talk
Structural Subtyping as Parametric Polymorphism
SPLASH OOPSLA
Wenhao Tang University of Edinburgh, Daniel Hillerström Huawei Zurich Research Center, James McKinna Heriot-Watt University, Michel Steuwer TU Berlin; University of Edinburgh, Ornela Dardha University of Glasgow, Rongxiao Fu University of Edinburgh, Sam Lindley University of Edinburgh
DOI Pre-print
14:36
18m
Talk
Simple Reference Immutability for System F<:
SPLASH OOPSLA
Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo
DOI
14:54
18m
Talk
Mutually Iso-Recursive Subtyping
SPLASH OOPSLA
Andreas Rossberg Independent
DOI
15:12
18m
Talk
Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference
SPLASH OOPSLA
Ishan Bhanuka Hong Kong University of Science and Technology, Lionel Parreaux Hong Kong University of Science and Technology, David Binder University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
DOI Pre-print
16:00 - 17:30
effect systemsSPLASH OOPSLA at Room I
Chair(s): Sebastian Erdweg JGU Mainz
16:00
18m
Talk
Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems
SPLASH OOPSLA
Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University, Troels Henriksen University of Copenhagen
DOI
16:18
18m
Talk
From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers
SPLASH OOPSLA
Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Lindegaard Starup Aarhus University, Klaus Ostermann University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
Link to publication DOI Pre-print
16:36
18m
Talk
Gradual Typing for Effect Handlers
SPLASH OOPSLA
Max S. New University of Michigan, Eric Giovannini University of Michigan, Daniel R. Licata Wesleyan University
DOI
16:54
18m
Talk
When Concurrency Matters: Behaviour-Oriented Concurrency
SPLASH OOPSLA
Luke Cheeseman Imperial College London, Matthew J. Parkinson Microsoft Azure Research, Sylvan Clebsch Microsoft Azure Research, Marios Kogias Imperial College London; Microsoft Research, Sophia Drossopoulou Imperial College London, David Chisnall Microsoft, Tobias Wrigstad Uppsala University, Paul Liétar Imperial College London
DOI
17:12
18m
Talk
Continuing WebAssembly with Effect Handlers
SPLASH OOPSLA
Luna Phipps-Costin Northeastern University, Andreas Rossberg Independent, Arjun Guha Northeastern University; Roblox, Daan Leijen Microsoft Research, Daniel Hillerström Huawei Zurich Research Center, KC Sivaramakrishnan Tarides; IIT Madras, Matija Pretnar University of Ljubljana, Sam Lindley University of Edinburgh
DOI Pre-print
17:30 - 17:45
Sponsored TalksSPLASH Sponsored Talks at Room I
Chair(s): Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon
17:30
15m
Talk
Programming Languages at Huawei
SPLASH Sponsored Talks
A: Dan Ghica Huawei

Fri 27 Oct

Displayed time zone: Lisbon change

09:00 - 09:30
AnnouncementsSPLASH OOPSLA at Room I
Chair(s): Vasco T. Vasconcelos LASIGE, University of Lisbon
  • Most Influential Paper Award
  • Student Research Competition Award
  • Artifact Evaluation Chair Report, including Distinguished OOPSLA Artifacts and Distinguished AEC Reviewers
  • SPLASH 2024 Pitch
09:30 - 10:30
Keynote 3SPLASH OOPSLA at Room I
Chair(s): Mira Mezini TU Darmstadt
09:30
60m
Keynote
All the Languages TogetherKeynote
SPLASH OOPSLA
Amal Ahmed Northeastern University, USA
11:00 - 12:30
verification 1SPLASH OOPSLA at Room I
Chair(s): Gowtham Kaki University of Colorado at Boulder
11:00
18m
Talk
Solving Conditional Linear Recurrences for Program Verification: The Periodic Case
SPLASH OOPSLA
Chenglin Wang Hong Kong University of Science and Technology, Fangzhen Lin Hong Kong University of Science and Technology
DOI
11:18
18m
Talk
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
SPLASH OOPSLA
Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Johannes Hostert ETH Zurich, Simon Spies MPI-SWS, Michael Sammler MPI-SWS, Lars Birkedal Aarhus University, Derek Dreyer MPI-SWS
Link to publication DOI
11:36
18m
Talk
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
SPLASH OOPSLA
Noam Zilberstein Cornell University, Derek Dreyer MPI-SWS, Alexandra Silva Cornell University
DOI Pre-print
11:54
18m
Talk
Formal Abstractions for Packet SchedulingDistinguished Paper
SPLASH OOPSLA
Anshuman Mohan Cornell University, Yunhe Liu Cornell University, Nate Foster Cornell University, Tobias Kappé Open University of the Netherlands; University of Amsterdam, Dexter Kozen Cornell University
Link to publication DOI
12:12
18m
Talk
P4R-Type: A Verified API for P4 Control Plane Programs
SPLASH OOPSLA
Jens Kanstrup Larsen DTU, Roberto Guanciale KTH Royal Institute of Technology, Philipp Haller KTH Royal Institute of Technology, Alceste Scalas DTU
DOI Pre-print Media Attached
14:00 - 15:30
verification 2SPLASH OOPSLA at Room I
Chair(s): Jonathan Aldrich Carnegie Mellon University
14:00
18m
Talk
Stuttering for Free
SPLASH OOPSLA
Minki Cho Seoul National University, Youngju Song MPI-SWS, Dongjae Lee Seoul National University, Lennard Gäher MPI-SWS, Derek Dreyer MPI-SWS
DOI
14:18
18m
Talk
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier
SPLASH OOPSLA
Zhengyao Lin Carnegie Mellon University, Xiaohong Chen University of Illinois at Urbana-Champaign, Minh-Thai Trinh Advanced Digital Sciences Center, John Wang University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
DOI
14:36
18m
Talk
Complete First-Order Reasoning for Properties of Functional Programs
SPLASH OOPSLA
Adithya Murali University of Illinois at Urbana-Champaign, Lucas Peña University of Illinois at Urbana-Champaign, Ranjit Jhala University of California at San Diego, P. Madhusudan University of Illinois at Urbana-Champaign
DOI
14:54
18m
Talk
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols
SPLASH OOPSLA
Orr Tamir Tel Aviv University, Marcelo Taube Tel Aviv University, Kenneth L. McMillan University of Texas at Austin, Sharon Shoham Tel Aviv University, Jon Howell VMware Research, Guy Gueta VMware Research, Mooly Sagiv Tel Aviv University
DOI
15:12
18m
Talk
A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model
SPLASH OOPSLA
Clément Blaudeau Inria, Fengyun Liu Oracle Labs
Link to publication DOI
16:00 - 17:30
distribution & networking 2SPLASH OOPSLA at Room I
Chair(s): Elisa Gonzalez Boix Vrije Universiteit Brussel
16:00
18m
Talk
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
SPLASH OOPSLA
Lorenzo Gheri University of Liverpool, Nobuko Yoshida University of Oxford
DOI
16:18
18m
Talk
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity
SPLASH OOPSLA
Chuta Sano McGill University, Ryan Kavanagh McGill University, Brigitte Pientka McGill University
DOI
16:36
18m
Talk
Message Chains for Distributed System Verification
SPLASH OOPSLA
Federico Mora University of California at Berkeley, Ankush Desai Amazon Web Services, Elizabeth Polgreen University of Edinburgh, Sanjit A. Seshia University of California at Berkeley
DOI
16:54
18m
Talk
Randomized Testing of Byzantine Fault Tolerant AlgorithmsDistinguished Paper
SPLASH OOPSLA
Levin N. Winter Delft University of Technology, Florena Buse Delft University of Technology, Daan de Graaf Delft University of Technology, Klaus von Gleissenthall Vrije Universiteit Amsterdam, Burcu Kulahcioglu Ozkan Delft University of Technology
DOI
17:12
18m
Talk
Validating IoT Devices with Rate-Based Session Types
SPLASH OOPSLA
Grant Iraci University at Buffalo, Cheng-En Chuang University at Buffalo, Raymond Hu Queen Mary University of London, Lukasz Ziarek University at Buffalo
DOI

Sun 22 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:0030
Room I

Mon 23 Oct

Displayed time zone: Lisbon change

Tue 24 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:0030
Room I

Wed 25 Oct

Displayed time zone: Lisbon change

Fri 27 Oct

Displayed time zone: Lisbon change

Sun 22 Oct

Displayed time zone: Lisbon change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:00153045
Room I
SAS
Opening
09:00 - 09:05

Tue 24 Oct

Displayed time zone: Lisbon change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:00153045
Room I

Wed 25 Oct

Displayed time zone: Lisbon change

Fri 27 Oct

Displayed time zone: Lisbon change