Room I - SPLASH 2023

VenueHotel Cascais Miragem

Room nameRoom I

Floor0

Capacity392

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT+01:00) Lisbon.

Use conference time zone: (GMT+01:00) LisbonSelect 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

Save

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 PostersPosters at Room I Chair(s): Xujie Si University of Toronto

17:30 2h Poster		Sui Move: Modern Blockchain Programming with Objects Posters Adam Welc Mysten Labs, Sam Blackshear Mysten Labs
17:30 2h Poster		Safe Combination of Data-centric and Operation-centric Consistency Posters Mirko Köhler TU Darmstadt, Guido Salvaneschi University of St. Gallen
17:30 2h Poster		Dynamic Library Compartmentalization Posters Octave Larose University of Kent
17:30 2h Poster		Collabs implements collaborative data structures (CRDTs) with OOP principles 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 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 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 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 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 Posters Sam Estep Carnegie Mellon University
17:30 2h Poster		JaMaBuild: Mass Building of Java Projects 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 Posters Tobias Reinhard KU Leuven, Justus Fasse Université Grenoble-Alpes; KU Leuven, Bart Jacobs KU Leuven
17:30 2h Poster		Towards Reusable GUI Structures 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 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 Posters Rijul Jain Williams College, Wode Ni Columbia University, Joshua Sunshine Carnegie Mellon University

Mon 23 Oct
Displayed time zone: Lisbon change

09:00 - 10:30	Session 5SAS at Room I Chair(s): Enea Zaffanella University of Parma, Italy

09:00 60m Keynote		Abstract Interpretation in Industry - Experience and Lessons LearnedKeynote SAS I: Daniel Kaestner AbsInt Pre-print
10:00 30m Talk		Lifting On-Demand Analysis to Higher-Order Languages SAS Daniel Schoepe Amazon, David Seekatz Unaffiliated, Ilina Stoilkovska Amazon, Sandro Stucki Amazon, Daniel Tattersall Amazon, Pauline Bolignano Amazon, Franco Raimondi Amazon, Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon Link to publication Pre-print

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 PostersPosters at Room I

17:30 8m Poster		Extensible Testing for Infrastructure as Code 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 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 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 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 Posters Matthew Weidner Carnegie Mellon University
18:12 8m Poster		Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs Posters Tobias Reinhard KU Leuven, Justus Fasse Université Grenoble-Alpes; KU Leuven, Bart Jacobs KU Leuven
18:21 8m Poster		Dynamic Library Compartmentalization Posters Octave Larose University of Kent
18:30 8m Poster		JaMaBuild: Mass Building of Java Projects 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 Posters Adam Welc Mysten Labs, Sam Blackshear Mysten Labs
18:47 8m Poster		Towards Reusable GUI Structures 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 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 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 Posters Mirko Köhler TU Darmstadt, Guido Salvaneschi University of St. Gallen
19:21 8m Poster		Penrose: Beautiful diagrams from plain text Posters Sam Estep Carnegie Mellon University

Wed 25 Oct
Displayed time zone: Lisbon change

09:00 - 09:30	Opening and WelcomeOOPSLA 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 OOPSLA

09:30 - 10:30	Keynote 1OOPSLA at Room I

09:30 60m Keynote		Scaling up machine learning without tears (and what do programming languages have to do with it)Keynote OOPSLA Dimitrios Vytiniotis Google DeepMind

11:00 - 12:30	AI4SEOOPSLA at Room I Chair(s): Guido Salvaneschi University of St. Gallen

11:00 18m Talk		Grounded Copilot: How Programmers Interact with Code-Generating Models 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 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 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 OOPSLA Yu Wang Nanjing University, Ke Wang , Linzhang Wang Nanjing University DOI
12:12 18m Talk		Optimization-Aware Compiler-Level Event Profiling 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	SE4AIOOPSLA 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 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 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 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-theorem 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 OOPSLA Yuval Shapira Technion, Eran Avneri Technion, Dana Drachsler Cohen Technion DOI

16:00 - 17:30	probabilisticOOPSLA at Room I Chair(s): Chandrakana Nandi Certora

16:00 18m Talk		A Deductive Verification Infrastructure for Probabilistic Programs 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 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 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 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 Stabilization 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 2OOPSLA at Room I Chair(s): Mira Mezini TU Darmstadt

09:30 60m Keynote		Hydroflow: A Compiler Target for Fast, Correct Distributed ProgramsKeynote OOPSLA Joseph M. Hellerstein UC Berkeley

11:00 - 12:30	type systems 1OOPSLA at Room I Chair(s): Max S. New University of Michigan

11:00 18m Talk		Reference Capabilities for Flexible Memory Management 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 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 OOPSLA Narges Shadab University of California at Riverside, PRITAM MANOHAR 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 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 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 2OOPSLA at Room I Chair(s): Max S. New University of Michigan

14:00 18m Talk		Greedy Implicit Bounded Quantification 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 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<: OOPSLA Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo DOI
14:54 18m Talk		Mutually Iso-Recursive Subtyping OOPSLA Andreas Rossberg Independent DOI
15:12 18m Talk		Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference 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 systemsOOPSLA 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 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 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 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 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 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 TalksSponsored Talks at Room I Chair(s): Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon

17:30 15m Talk		Programming Languages at Huawei Sponsored Talks A: Dan Ghica Huawei

Fri 27 Oct
Displayed time zone: Lisbon change

	09:00 - 09:30	AnnouncementsOOPSLA 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 3OOPSLA at Room I Chair(s): Mira Mezini TU Darmstadt

09:30 60m Keynote		All the Languages TogetherKeynote OOPSLA Amal Ahmed Northeastern University, USA

11:00 - 12:30	verification 1OOPSLA 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 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 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 OOPSLA Noam Zilberstein Cornell University, Derek Dreyer MPI-SWS, Alexandra Silva Cornell University DOI Pre-print
11:54 18m Talk		Formal Abstractions for Packet Scheduling 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 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 2OOPSLA at Room I Chair(s): Jonathan Aldrich Carnegie Mellon University

14:00 18m Talk		Stuttering for Free 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 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 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 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 OOPSLA Clément Blaudeau Inria, Fengyun Liu Oracle Labs Link to publication DOI

16:00 - 17:30	distribution & networking 2OOPSLA 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 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 OOPSLA Chuta Sano McGill University, Ryan Kavanagh McGill University, Brigitte Pientka McGill University DOI
16:36 18m Talk		Message Chains for Distributed System Verification 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 Algorithms 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 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


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
Room I	SAS Session 1																								SAS Domain precision																																				SAS Synthesis and applications																								SAS Quantum, neural																		MPLR MPLR Posters Posters SPLASH Posters 17:30 - 19:30

Mon 23 Oct
Displayed time zone: Lisbon 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
Room I	SAS Session 5																								SAS Modular arithmetic and numeric analysis																																				SAS Error location and scaling																								SAS Session 8

Tue 24 Oct
Displayed time zone: Lisbon 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
Room I	SAS Cost/precision trade-offs and acceleration																								SAS Session 10																																				SAS																								SAS																		Posters SPLASH Posters MPLR 17:30 - 19:30

Wed 25 Oct
Displayed time zone: Lisbon 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
Room I	OOPSLA Opening and Welcome						OOPSLA Keynote 1																		OOPSLA AI4SE																																				OOPSLA SE4AI																								OOPSLA probabilistic

Thu 26 Oct
Displayed time zone: Lisbon 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
Room I				OOPSLA			OOPSLA Keynote 2																		OOPSLA type systems 1																																				OOPSLA type systems 2																								OOPSLA effect systems																		Sponsored Talks Sponsored Talks

Fri 27 Oct
Displayed time zone: Lisbon 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
Room I	OOPSLA Announcements						OOPSLA Keynote 3																		OOPSLA verification 1																																				OOPSLA verification 2																								OOPSLA distribution & networking 2

Sun 22 Oct
Displayed time zone: Lisbon 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
Room I	SAS Opening 09:00 - 09:05	SAS Keynote Goal-Directed Abstract Interpretation and Event-Driven Frameworks 09:05 - 10:05												SAS A Product of Shape and Sequence Abstractions (Radhia Cousot Young Rese ... 10:05 - 10:35											SAS How fitting is your abstract domain? 11:00 - 11:30						SAS Domain Precision in Galois Connection-less Abstract Interpretation 11:30 - 12:00						SAS A Formal Framework to Measure the Incompleteness of Abstract Interpreta ... 12:00 - 12:30																								SAS Generalized Program Sketching by Abstract Interpretation and Logical Ab ... 14:00 - 14:30						SAS Reverse Template Processing using Abstract Interpretation 14:30 - 15:00						SAS Remote BREWasm: A General Static Binary Rewriting Framework for WebAssembly 15:00 - 15:30												SAS Quantum Constant Propagation 16:00 - 16:30						SAS Boosting Multi-Neuron Convex Relaxation for Neural Network Verification 16:30 - 17:00												MPLR CloudJIT: A Just-in-Time FaaS Optimizer (Poster Abstract) 17:30 - 18:10 SPLASH Posters Sui Move: Modern Blockchain Programming with Objects 17:30 - 19:30 Safe Combination of Data-centric and Operation-centric Consistency 17:30 - 19:30 Dynamic Library Compartmentalization 17:30 - 19:30 Collabs implements collaborative data structures (CRDTs) with OOP princ ... 17:30 - 19:30 Involving Users in Design of a Widely Used Language: A Case of ECMAScri ... 17:30 - 19:30 A Functional Reactive Programming Language for Wirelessly Connected Sha ... 17:30 - 19:30 Kind Inference for the FreeST Programming Language 17:30 - 19:30 Extensible Testing for Infrastructure as Code 17:30 - 19:30 Penrose: Beautiful diagrams from plain text 17:30 - 19:30 JaMaBuild: Mass Building of Java Projects 17:30 - 19:30 Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bou ... 17:30 - 19:30 Towards Reusable GUI Structures 17:30 - 19:30 ReactCOP: Modular and Scalable Web Development with Context-Oriented Pr ... 17:30 - 19:30 Generating Domain-Specific Programs for Diagram Authoring with Large La ... 17:30 - 19:30								MPLR Don’t Trust Your Profiler: An Empirical Study on the Precision and Accu ... 18:10 - 18:50								MPLR Diagnosing Compiler Performance by Comparing Optimization Decisions (Po ... 18:50 - 19:30

Mon 23 Oct
Displayed time zone: Lisbon 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
Room I	SAS Keynote Abstract Interpretation in Industry - Experience and Lessons Learned 09:00 - 10:00												SAS Lifting On-Demand Analysis to Higher-Order Languages 10:00 - 10:30												SAS Symbolic transformation of expressions in modular arithmetic 11:00 - 11:30						SAS Polynomial Analysis of Modular Arithmetic 11:30 - 12:00						SAS Octagons Revisited - Elegant Proofs and Simplified Algorithms 12:00 - 12:30																								SAS Error Invariants for Fault Localization via Abstract Interpretation 14:00 - 14:30						SAS Error Localization for Sequential Effect Systems 14:30 - 15:00						SAS Scaling up Roundoff Analysis of Functional Data Structure Programs 15:00 - 15:30												SAS RemoteKeynote Building Trust and Safety in Artificial Intelligence with Abstract Inte ... 16:00 - 17:00												SAS Radhia Cousot Award and PC report 17:00 - 17:30

Tue 24 Oct
Displayed time zone: Lisbon 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
Room I	SAS ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses 09:00 - 09:30						SAS Unconstrained Variable Oracles for Faster Static Analyses 09:30 - 10:00						SAS Modular Optimization-Based Roundoff Error Analysis of Floating-Point Pr ... 10:00 - 10:30												SAS Keynote Verifying Infinitely Many Programs at Once 11:00 - 12:00												SAS Mutual Refinements of Context-Free Language Reachability 12:00 - 12:30																																																																		SPLASH Posters Extensible Testing for Infrastructure as Code 17:30 - 17:38		SPLASH Posters ReactCOP: Modular and Scalable Web Development with Context-Oriented Pr ... 17:38 - 17:47	SPLASH Posters Involving Users in Design of a Widely Used Language: A Case of ECMAScri ... 17:47 - 17:55		SPLASH Posters Kind Inference for the FreeST Programming Language 17:55 - 18:04		SPLASH Posters Collabs implements collaborative data structures (CRDTs) with OOP princ ... 18:04 - 18:12	SPLASH Posters Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bou ... 18:12 - 18:21		SPLASH Posters Dynamic Library Compartmentalization 18:21 - 18:30		SPLASH Posters JaMaBuild: Mass Building of Java Projects 18:30 - 18:38		SPLASH Posters Sui Move: Modern Blockchain Programming with Objects 18:38 - 18:47	SPLASH Posters Towards Reusable GUI Structures 18:47 - 18:55		SPLASH Posters A Functional Reactive Programming Language for Wirelessly Connected Sha ... 18:55 - 19:04		SPLASH Posters Generating Domain-Specific Programs for Diagram Authoring with Large La ... 19:04 - 19:12	SPLASH Posters Safe Combination of Data-centric and Operation-centric Consistency 19:12 - 19:21		SPLASH Posters Penrose: Beautiful diagrams from plain text 19:21 - 19:30

Wed 25 Oct
Displayed time zone: Lisbon 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
Room I	SPLASH OOPSLA Opening and Welcome 09:00 - 09:30						SPLASH OOPSLAKeynote Scaling up machine learning without tears (and what do programming lang ... 09:30 - 10:30																		SPLASH OOPSLA Grounded Copilot: How Programmers Interact with Code-Generating Models 11:00 - 11:18				SPLASH OOPSLA Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates ... 11:18 - 11:36			SPLASH OOPSLA Concrete Type Inference for Code Optimization using Machine Learning wi ... 11:36 - 11:54				SPLASH OOPSLA An Explanation Method for Models of Code 11:54 - 12:12			SPLASH OOPSLA Optimization-Aware Compiler-Level Event Profiling 12:12 - 12:30																						SPLASH OOPSLA Run-Time Prevention of Software Integration Failures of Machine Learnin ... 14:00 - 14:18				SPLASH OOPSLA Compiling Structured Tensor Algebra 14:18 - 14:36			SPLASH OOPSLA Perception Contracts for Safety of ML-Enabled Systems 14:36 - 14:54				SPLASH OOPSLA Languages with Decidable Learning: A Meta-theorem 14:54 - 15:12			SPLASH OOPSLA Deep Learning Robustness Verification for Few-Pixel Attacks 15:12 - 15:30										SPLASH OOPSLA A Deductive Verification Infrastructure for Probabilistic Programs 16:00 - 16:18				SPLASH OOPSLA A Gradual Probabilistic Lambda Calculus 16:18 - 16:36			SPLASH OOPSLA Lower Bounds for Possibly Divergent Probabilistic Programs 16:36 - 16:54				SPLASH OOPSLA Exact Recursive Probabilistic Programming 16:54 - 17:12			SPLASH OOPSLA Solving String Constraints with Lengths by Stabilization 17:12 - 17:30

Thu 26 Oct
Displayed time zone: Lisbon 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
Room I							SPLASH OOPSLAKeynote Hydroflow: A Compiler Target for Fast, Correct Distributed Programs 09:30 - 10:30																		SPLASH OOPSLA Reference Capabilities for Flexible Memory Management 11:00 - 11:18				SPLASH OOPSLA A Grounded Conceptual Model for Ownership Types in Rust 11:18 - 11:36			SPLASH OOPSLA Inference of Resource Management Specifications 11:36 - 11:54				SPLASH OOPSLA Resource-Aware Soundness for Big-Step Semantics 11:54 - 12:12			SPLASH OOPSLA Verus: Verifying Rust Programs using Linear Ghost Types 12:12 - 12:30																						SPLASH OOPSLA Greedy Implicit Bounded Quantification 14:00 - 14:18				SPLASH OOPSLA Structural Subtyping as Parametric Polymorphism 14:18 - 14:36			SPLASH OOPSLA Simple Reference Immutability for System F<: 14:36 - 14:54				SPLASH OOPSLA Mutually Iso-Recursive Subtyping 14:54 - 15:12			SPLASH OOPSLA Getting into the Flow: Towards Better Type Error Messages for Constrain ... 15:12 - 15:30										SPLASH OOPSLA Fast and Efficient Boolean Unification for Hindley-Milner-Style Type an ... 16:00 - 16:18				SPLASH OOPSLA From Capabilities to Regions: Enabling Efficient Compilation of Lexical ... 16:18 - 16:36			SPLASH OOPSLA Gradual Typing for Effect Handlers 16:36 - 16:54				SPLASH OOPSLA When Concurrency Matters: Behaviour-Oriented Concurrency 16:54 - 17:12			SPLASH OOPSLA Continuing WebAssembly with Effect Handlers 17:12 - 17:30				SPLASH Sponsored Talks Programming Languages at Huawei 17:30 - 17:45

Fri 27 Oct
Displayed time zone: Lisbon 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
Room I							SPLASH OOPSLAKeynote All the Languages Together 09:30 - 10:30																		SPLASH OOPSLA Solving Conditional Linear Recurrences for Program Verification: The Pe ... 11:00 - 11:18				SPLASH OOPSLA Melocoton: A Program Logic for Verified Interoperability Between OCaml ... 11:18 - 11:36			SPLASH OOPSLA Outcome Logic: A Unifying Foundation for Correctness and Incorrectness ... 11:36 - 11:54				SPLASH OOPSLA Formal Abstractions for Packet Scheduling 11:54 - 12:12			SPLASH OOPSLA P4R-Type: A Verified API for P4 Control Plane Programs 12:12 - 12:30																						SPLASH OOPSLA Stuttering for Free 14:00 - 14:18				SPLASH OOPSLA Generating Proof Certificates for a Language-Agnostic Deductive Program ... 14:18 - 14:36			SPLASH OOPSLA Complete First-Order Reasoning for Properties of Functional Programs 14:36 - 14:54				SPLASH OOPSLA Counterexample Driven Quantifier Instantiations with Applications to Di ... 14:54 - 15:12			SPLASH OOPSLA A conceptual framework for safe object initialization: a principled and ... 15:12 - 15:30										SPLASH OOPSLA Hybrid Multiparty Session Types: Compositionality for Protocol Specific ... 16:00 - 16:18				SPLASH OOPSLA Mechanizing Session-Types using a Structural View: Enforcing Linearity ... 16:18 - 16:36			SPLASH OOPSLA Message Chains for Distributed System Verification 16:36 - 16:54				SPLASH OOPSLA Randomized Testing of Byzantine Fault Tolerant Algorithms 16:54 - 17:12			SPLASH OOPSLA Validating IoT Devices with Rate-Based Session Types 17:12 - 17:30

Room information: Room I

Program Display Configuration

Sun 22 OctDisplayed time zone: Lisbon change

Mon 23 OctDisplayed time zone: Lisbon change

Tue 24 OctDisplayed time zone: Lisbon change

Wed 25 OctDisplayed time zone: Lisbon change

Thu 26 OctDisplayed time zone: Lisbon change

Fri 27 OctDisplayed time zone: Lisbon change

Sun 22 OctDisplayed time zone: Lisbon change

SAS

SAS

SAS

SAS

MPLR

Posters

Mon 23 OctDisplayed time zone: Lisbon change

SAS

SAS

SAS

SAS

Tue 24 OctDisplayed time zone: Lisbon change

SAS

SAS

SAS

SAS

Posters

MPLR

Wed 25 OctDisplayed time zone: Lisbon change

OOPSLA

OOPSLA

OOPSLA

OOPSLA

OOPSLA

Thu 26 OctDisplayed time zone: Lisbon change

OOPSLA

OOPSLA

OOPSLA

OOPSLA

OOPSLA

Sponsored Talks

Fri 27 OctDisplayed time zone: Lisbon change

OOPSLA

OOPSLA

OOPSLA

OOPSLA

OOPSLA

Sun 22 OctDisplayed time zone: Lisbon change

Mon 23 OctDisplayed time zone: Lisbon change

Tue 24 OctDisplayed time zone: Lisbon change

Wed 25 OctDisplayed time zone: Lisbon change

Thu 26 OctDisplayed time zone: Lisbon change

Fri 27 OctDisplayed time zone: Lisbon change

Sun 22 Oct
Displayed time zone: Lisbon change

Mon 23 Oct
Displayed time zone: Lisbon change

Tue 24 Oct
Displayed time zone: Lisbon change

Wed 25 Oct
Displayed time zone: Lisbon change

Thu 26 Oct
Displayed time zone: Lisbon change

Fri 27 Oct
Displayed time zone: Lisbon change

Sun 22 Oct
Displayed time zone: Lisbon change

Mon 23 Oct
Displayed time zone: Lisbon change

Tue 24 Oct
Displayed time zone: Lisbon change

Wed 25 Oct
Displayed time zone: Lisbon change

Thu 26 Oct
Displayed time zone: Lisbon change

Fri 27 Oct
Displayed time zone: Lisbon change

Sun 22 Oct
Displayed time zone: Lisbon change

Mon 23 Oct
Displayed time zone: Lisbon change

Tue 24 Oct
Displayed time zone: Lisbon change

Wed 25 Oct
Displayed time zone: Lisbon change

Thu 26 Oct
Displayed time zone: Lisbon change

Fri 27 Oct
Displayed time zone: Lisbon change