SPLASH 2023 - OOPSLA - SPLASH 2023

This program is tentative and subject to change.

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

Wed 25 Oct
Displayed time zone: Lisbon change

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

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

	10:30 - 11:00	Coffee BreakCatering at I + II foyer

11:00 - 12:30	AI4SEOOPSLA at Room I

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		Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network OOPSLA Shangwen Wang National University of Defense Technology, Bo Lin National University of Defense Technology, Zhensu Sun Singapore Management University, Ming Wen Huazhong University of Science and Technology, Yepang Liu Southern University of Science and Technology, Yan Lei Chongqing University, Xiaoguang Mao National University of Defense Technology DOI Pre-print
11:36 18m Talk		Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs OOPSLA Alex Renda Massachusetts Institute of Technology, Yi Ding Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology Pre-print
11:54 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
12:12 18m Talk		An Explanation Method for Models of Code OOPSLA Yu WANG Nanjing University, Ke Wang Visa Research, Linzhang Wang Nanjing University

11:00 - 12:30	program synthesis 1OOPSLA at Room II

11:00 18m Talk		Asparagus: Automated Synthesis of Parametric Gas Upper-bounds for Smart Contracts OOPSLA Zhuo Cai Hong Kong University of Science and Technology, Soroush Farokhnia Hong Kong University of Science and Technology, Amir Kafshdar Goharshady IST Austria, Austria, S. Hitarth Hong Kong University of Science and Technology
11:18 18m Talk		Equality Saturation Theory Exploration à la Carte OOPSLA Anjali Pal University of Washington, Brett Saiki University of Washington, Oliver Flatt , Ryan Tjoa University of Washington, Amy Zhu University of Washington, Cynthia Richey University of Washington, Max Willsey University of California, Berkeley, Zachary Tatlock University of Washington, Chandrakana Nandi Certora Pre-print
11:36 18m Talk		Synthesizing Specifications OOPSLA Kanghee Park University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison
11:54 18m Talk		Explainable Program Synthesis by Localizing Specifications OOPSLA Amirmohammad Nazari University of Southern California, Yifei Huang University of Southern California, Roopsha Samanta Purdue University, Arjun Radhakrishna Microsoft, Mukund Raghothaman University of Southern California
12:12 18m Talk		Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction OOPSLA Zhenyang Xu University of Waterloo, Yongqiang Tian The Hong Kong University of Science and Technology; University of Waterloo, Mengxiao Zhang University of Waterloo, Gaosen Zhao University of Waterloo, Yu Jiang Tsinghua University, Chengnian Sun University of Waterloo DOI

	14:00 - 18:00	LunchCatering at Gallery

14:00 - 15:30	SE4AIOOPSLA at Room I

14:00 18m Talk		Deep Learning Robustness Verification for Few-Pixel Attacks OOPSLA Yuval Shapira Technion, Eran Avneri Technion, Dana Drachsler Cohen Technion DOI
14:18 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 University of Chicago
14:36 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
14:54 18m Talk		Perception Contracts for Safety of ML-Enabled Systems OOPSLA Angello Astorga University of Illinois at Urbana-Champaign, Chiao Hsieh Graduate School of Informatics, Kyoto University, P. Madhusudan University of Illinois at Urbana-Champaign, Sayan Mitra University of Illinois at Urbana-Champaign
15:12 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

14:00 - 15:30	program synthesis 2OOPSLA at Room II

14:00 18m Talk		Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates OOPSLA Aalok Thakkar University of Pennsylvania, Nathaniel Sands University of Southern California, Georgios Petrou University of Southern California, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania, Mukund Raghothaman University of Southern California
14:18 18m Talk		Data Extraction via Semantic Regular Expression Synthesis OOPSLA Qiaochu Chen University of Texas at Austin, Arko Banerjee University of Texas at Austin, Çağatay Demiralp MIT CSAIL, Greg Durrett University of Texas at Austin, Işil Dillig University of Texas at Austin
14:36 18m Talk		Synthesizing Efficient Memoization Algorithms OOPSLA Yican Sun Peking University, Xuanyu Peng Peking University, Yingfei Xiong Peking University
14:54 18m Talk		Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs OOPSLA Amir Kafshdar Goharshady Hong Kong University of Science and Technology, S. Hitarth Hong Kong University of Science and Technology, Fatemeh Mohammadi KU Leuven, Harshit Jitendra Motwani Ghent University DOI
15:12 18m Talk		Modular Component-Based Quantum Circuit Synthesis OOPSLA Chan Gu Kang Korea University, Hakjoo Oh Korea University DOI

	15:30 - 16:00	Coffee BreakCatering at I + II foyer

16:00 - 17:30	probabilisticOOPSLA at Room I

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
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 DOI
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, Taiwan, David Chocholatý Brno University of Technology, Czech Republic, 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, Czech Republic

16:00 - 17:30	DSLsOOPSLA at Room II

16:00 15m Talk		Fluent APIs in Functional Languages OOPSLA Ori Roth Technion, Yossi Gil Technion DOI Pre-print
16:15 15m Talk		Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid OOPSLA Huanqi Cao Tsinghua University, Shizhi Tang Tsinghua University, Qianchao Zhu Peking University, Bowen Yu Nanjing University, Wenguang Chen Tsinghua University
16:30 15m Talk		How Domain Experts Use an Embedded DSL OOPSLA Lisa Rennels UC Berkeley, Sarah E. Chasins University of California at Berkeley
16:45 15m Talk		Saggitarius: A DSL for Specifying Grammatical Domains OOPSLA Anders Miltner Simon Fraser University, Devon Loehr Princeton University, Arnold Mong Princeton University, Kathleen Fisher Tufts University, David Walker Princeton University
17:00 15m Talk		A Pretty Expressive Printer OOPSLA Sorawee Porncharoenwase University of Washington, Justin Pombrio Brown University, USA, Emina Torlak Amazon Web Services and University of Washington Pre-print
17:15 15m Talk		Translating canonical SQL to imperative code in Coq OOPSLA Véronique Benzaken Université Paris-Saclay - Laboratoire de Méthodes Formelles , Évelyne Contejean CNRS, ENS Paris-Saclay & Université Paris-Saclay, Houssem Hachmaoui , Chantal Keller Université Paris Saclay, Louis Mandel IBM Research, USA, Avraham Shinnar IBM Research, Jerome Simeon DocuSign, Inc. Link to publication DOI

Thu 26 Oct
Displayed time zone: Lisbon change

09:00 - 10:30	Keynote 2OOPSLA at Room I

09:00 90m Keynote		Thursday Keynote (Title Placeholder) OOPSLA Joseph M. Hellerstein UC Berkeley

	10:30 - 11:00	Coffee BreakCatering at I + II foyer

11:00 - 12:30	type systems 1OOPSLA at Room I

11:00 18m Talk		Reference Capabilities for Flexible Memory Management OOPSLA Ellen Arvidsson Uppsala University, Elias Castegren Uppsala University, Sylvan Clebsch Azure Research, Sophia Drossopoulou Imperial College London , James Noble Research & Programming, Matthew Parkinson Azure Research, Microsoft, UK, Tobias Wrigstad Uppsala University, Sweden
11:18 18m Talk		A Grounded Conceptual Model for Ownership Types in Rust OOPSLA Will Crichton Brown University, Gavin Gray ETH Zürich, Shriram Krishnamurthi Brown University, United States 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 India, 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
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
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

11:00 - 12:30	language semanticsOOPSLA at Room II

11:00 18m Talk		The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog OOPSLA Qinlin Chen Nanjing University, Nairen Zhang Nanjing University, Jinpeng Wang Nanjing University, Tian Tan Nanjing University, Chang Xu Nanjing University, Xiaoxing Ma Nanjing University, Yue Li Nanjing University
11:18 18m Talk		Regular Expression Matching using Bit Vector Automata OOPSLA Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University DOI
11:36 18m Talk		Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects OOPSLA Xing Zhang Peking University, Guanchen Guo Peking University, Xiao He University of Science and Technology Beijing, Zhenjiang Hu Peking University DOI
11:54 18m Talk		Bring Your Own Data Structures to Datalog OOPSLA Arash Sahebolamri Syracuse University, Langston Barrett Galois, Inc, Scott Moore Galois, Inc., Kristopher Micinski Syracuse University
12:12 18m Talk		Rhombus: A New Spin on Macros Without All the Parentheses OOPSLA Matthew Flatt University of Utah, Taylor Allred University of Utah, Ross Angle independent, Stephen De Gabrielle independent, Robby Findler Northwestern University, Jack Firth independent, Kiran Gopinathan National University of Singapore, Ben Greenman Brown University, Siddhartha Kasivajhula independent, Alex Knauth Northeastern University, Jay McCarthy University of Massachusetts Lowell & Reach, Sam Phillips independent, Sorawee Porncharoenwase University of Washington, Jens Axel Søgaard independent, Sam Tobin-Hochstadt Indiana University Pre-print

	12:30 - 14:00	LunchCatering at Gallery

14:00 - 15:30	type systems 2OOPSLA at Room I

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
14:18 18m Talk		Structural Subtyping as Parametric Polymorphism OOPSLA Wenhao Tang The University of Edinburgh, Daniel Hillerström Huawei Zurich Research Center, James McKinna Heriot-Watt University, Michel Steuwer Technische Universität Berlin / University of Edinburgh, Ornela Dardha University of Glasgow, Rongxiao Fu The University of Edinburgh, Sam Lindley University of Edinburgh
14:36 18m Talk		Simple Reference Immutability for System F-Sub OOPSLA Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo
14:54 18m Talk		Mutually Iso-recursive Subtyping OOPSLA Andreas Rossberg Independent
15:12 18m Talk		Getting Into The Flow: Better Type Error Messages for Constraint-Based Type Inference OOPSLA Ishan Bhanuka HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux HKUST (The Hong Kong University of Science and Technology), David Binder University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen

14:00 - 15:30	program analysis 1OOPSLA at Room II

14:00 18m Talk		The Bounded Pathwidth of Control-flow Graphs OOPSLA Giovanna Kobus Conrado Hong Kong University of Science and Technology (HKUST), Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Chun Kit LAM Hong Kong University of Science and Technology (HKUST)
14:18 18m Talk		How Profilers Can Help Navigate Type Migration OOPSLA Ben Greenman Brown University, Matthias Felleisen PLT @ Northeastern University, Christos Dimoulas PLT @ Northwestern University
14:36 18m Talk		Synthesizing Precise Static Analyzers for Automatic Differentiation OOPSLA Jacob Laurel University of Illinois at Urbana-Champaign, Siyuan Brant Qian University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign
14:54 18m Talk		A Container-Usage-Pattern-based Context Debloating Approach for Object-Sensitive Pointer Analysis OOPSLA Dongjie He UNSW, Yujiang Gui UNSW Sydney, Wei Li University of New South Wales, Yonggang Tao University of New South Wales, Changwei Zou University of New South Wales, Yulei Sui University of New South Wales, Sydney, Jingling Xue UNSW
15:12 18m Talk		Static Analysis of Memory Models for SMT Encodings OOPSLA Thomas Haas Technical University of Braunschweig, René Maseli TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei Dresden Research Center

	15:30 - 16:00	Coffee BreakCatering at I + II foyer

16:00 - 17:30	effect systemsOOPSLA at Room I

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, Denmark
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
16:36 18m Talk		Gradual Typing for Effect Handlers OOPSLA Max New University of Michigan, Eric Giovannini University of Michigan, Dan Licata Wesleyan University
16:54 18m Talk		When Concurrency Matters: Behaviour-Oriented Concurrency OOPSLA Luke Cheeseman Imperial College London, Matthew Parkinson Azure Research, Microsoft, UK, Sylvan Clebsch Azure Research, Marios Kogias Imperial College London & Microsoft Research, Sophia Drossopoulou Imperial College London , David Chisnall , Tobias Wrigstad Uppsala University, Sweden, Paul Liétar Imperial College London
17:12 18m Talk		Continuing WebAssembly with Effect Handlers OOPSLA Luna Phipps-Costin Northeastern University, Andreas Rossberg Independent, Arjun Guha Northeastern University and Roblox Research, Daan Leijen Microsoft Research, Daniel Hillerström Huawei Zurich Research Center, KC Sivaramakrishnan IIT Madras and Tarides, Matija Pretnar University of Ljubljana, Slovenia, Sam Lindley University of Edinburgh Pre-print

16:00 - 17:30	program analysis 2OOPSLA at Room II

16:00 18m Talk		Historia: Refuting Callback Reachability with Message-History Logics OOPSLA Shawn Meier University of Colorado, Boulder, Sergio Mover Ecole Polytechnique, Gowtham Kaki University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
16:18 18m Talk		Exploiting the Sparseness of Control-flow and Call Graphs for Efficient and On-demand Algebraic Program Analysis OOPSLA Giovanna Kobus Conrado Hong Kong University of Science and Technology (HKUST), Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Kerim Kochekov Hong Kong University of Science and Technology, Yun Chen Tsai Hong Kong University of Science and Technology, Ahmed Khaled Zaher HKUST
16:36 18m Talk		A Cocktail Approach to Practical Call Graph Construction OOPSLA Yuandao Cai Hong Kong University of Science and Technology, China, Charles Zhang Hong Kong University of Science and Technology
16:54 18m Talk		Building Dynamic System Call Sandbox With Partial Order Analysis OOPSLA Quan Zhang Tsinghua University, Chijin Zhou Tsinghua University, Yiwen Xu Tsinghua University, Zijing Yin Tsinghua University, Mingzhe Wang Tsinghua University, Zhuo Su Tsinghua University, Chengnian Sun University of Waterloo, Yu Jiang Tsinghua University, Jiaguang Sun Tsinghua University
17:12 18m Talk		Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection OOPSLA Ruyi Ji Peking University, Chaozhe Kong Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University DOI

16:00 - 17:30	compilation & optimization 2OOPSLA at Room XII

16:00 18m Talk		Graph IRs for Impure Higher-Order Languages - Making Aggressive Optimizations Affordable with Precise Effect Dependencies OOPSLA Oliver Bračevac Galois, Inc., Guannan Wei Purdue University, Songlin Jia Purdue University, Supun Abeysinghe Purdue University, Yuxuan Jiang Purdue University, Yuyan Bao Computer and Cyber Sciences, Augusta University, Georgia, USA, Tiark Rompf Purdue University
16:18 18m Talk		AST vs. Bytecode: Interpreters in the Age of Meta-Compilation OOPSLA Octave Larose University of Kent, Sophie Kaleba University of Kent, Humphrey Burchell University of Kent, Stefan Marr University of Kent DOI Pre-print
16:36 18m Talk		Reusing Just-in-Time Compiled Code OOPSLA Meetesh Kalpesh Mehta Indian Institute of Technology Bombay, Sebastián Krynski Czech Technical University, Hugo Musso Gualandi Czech Technical University in Prague, Manas Thakur Indian Institute of Technology Bombay, Jan Vitek Northeastern University
16:54 18m Talk		TASTyTruffle: Just-in-time Specialization of Parametric Polymorphism OOPSLA Matt D'Souza University of Waterloo, James You University of Waterloo, Ondřej Lhoták University of Waterloo, Aleksandar Prokopec Oracle Labs
17:12 18m Talk		Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics OOPSLA Girish Mururu Georgia Institute of Technology, Sharjeel Khan Georgia Institute of Technology, Bodhisatwa Chatterjee Georgia Institute of Technology, Chao Chen Georgia Institute of Technology, Chris Porter Georgia Institute of Technology, USA, Ada Gavrilovska Georgia Institute of Technology, Santosh Pande Georgia Institute of Technology

Fri 27 Oct
Displayed time zone: Lisbon change

09:00 - 10:30	Keynote 3OOPSLA at Room I

09:00 90m Talk		Friday Keynote (Title Placeholder) OOPSLA Amal Ahmed Northeastern University, USA

	10:30 - 11:00	Coffee BreakCatering at I + II foyer

11:00 - 12:30	verification 1OOPSLA at Room I

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 , Johannes Hostert Saarland University, MPI-SWS, Simon Spies MPI-SWS, Michael Sammler MPI-SWS, Lars Birkedal Aarhus University, Derek Dreyer MPI-SWS
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 Universiteit of the Netherlands and ILLC, University of Amsterdam, Dexter Kozen Cornell University
12:12 18m Talk		P4R-Type: a Verified API for P4 Control Plane Programs OOPSLA Roberto Guanciale KTH, Alceste Scalas Technical University of Denmark, Philipp Haller KTH Royal Institute of Technology, Jens Kanstrup Larsen DTU DOI Pre-print Media Attached

11:00 - 12:30	distribution & networking 1OOPSLA at Room II

11:00 18m Talk		Initializing Global Objects: Time and Order OOPSLA Fengyun Liu Oracle Labs, Ondřej Lhoták University of Waterloo, David Hua University of Waterloo, Enze Xing University of Waterloo
11:18 18m Talk		Type-Safe Dynamic Placement with First-Class Placed Values OOPSLA George Zakhour University of St.Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen DOI Pre-print
11:36 18m Talk		Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data OOPSLA Thierry Renaux Vrije Universiteit Brussel, Sam Van den Vonder Vrije Universiteit Brussel, Wolfgang De Meuter Vrije Universiteit Brussel DOI Pre-print
11:54 18m Talk		AtomiS: Data-centric synchronization made practical OOPSLA Hervé Paulino NOVA University of Lisbon, Ana Matos University of Lisbon, Jan Cederquist University of Lisbon, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa, João Batista Pereira Matos Júnior Sidia Instituto de Ciência e Tecnologia, Antonio Ravara NOVA LINCS & FCT, NOVA University of Lisbon
12:12 18m Talk		Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions OOPSLA Christopher Wagner Purdue University, Nouraldin Jaber Purdue University, Roopsha Samanta Purdue University DOI

11:00 - 12:30	software developmentOOPSLA at Room XII

11:00 15m Talk		Towards Better Semantics Exploration for Browser Fuzzing OOPSLA Chijin Zhou Tsinghua University, Quan Zhang Tsinghua University, Lihua Guo Tsinghua University, Mingzhe Wang Tsinghua University, Yu Jiang Tsinghua University, Qing Liao Harbin Institute of Technology, Zhiyong Wu National University of Defense Technology, Shanshan Li National University of Defense Technology, Bin Gu Beijing Institute of Control Engineering, China
11:30 15m Talk		Live Pattern Matching with Typed Holes OOPSLA Yongwei Yuan Purdue University, Scott Guest University of Michigan, Eric Griffis University of Michigan, Hannah Potter University of Washington, David Moon University of Michigan, Cyrus Omar University of Michigan DOI
11:45 15m Talk		Interactive Debugging of Datalog Programs OOPSLA André Pacak JGU Mainz, Sebastian Erdweg JGU Mainz
12:00 15m Talk		Accelerating Fuzzing through Prefix-Guided Execution OOPSLA Shaohua Li ETH Zurich, Zhendong Su ETH Zurich DOI
12:15 15m Talk		MemPerf: Profiling Allocator-Induced Performance Slowdowns OOPSLA Jin Zhou University of Massachusetts Amherst, Sam Silvestro University of Texas at San Antonio, Jiaxun,Tang University of Massachusetts Amherst, Hanmei Yang University of Massachusetts Amherst, Hongyu Liu University of Texas at San Antonio, Guangming Zeng Synopsys, Bo Wu Colorado School of Mines, Cong Liu University of California at Riverside, Tongping Liu University of Massachusetts at Amherst

	12:30 - 14:00	LunchCatering at Gallery

14:00 - 15:30	verification 2OOPSLA at Room I

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 & Saarland University, Derek Dreyer MPI-SWS
14:18 18m Talk		Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks OOPSLA Pengfei Gao ShanghaiTech University, Yedi Zhang ShanghaiTech University, Fu Song ShanghaiTech University, Taolue Chen Birkbeck University of London, Francois-Xavier Standaert UCLouvain
14:36 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:54 18m Talk		Complete First-Order Reasoning for Properties of Functional Programs OOPSLA Adithya Murali University of Illinois at Urbana-Champaign, Lucas Pena , Ranjit Jhala University of California at San Diego, P. Madhusudan University of Illinois at Urbana-Champaign
15:12 18m Talk		Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols OOPSLA Orr Tamir Tel Aviv University, Marcelo Taube Tel Aviv University, Israel, Kenneth L. McMillan University of Texas at Austin, Sharon Shoham Tel Aviv University, Jon Howell VMware Research, Guy Gueta VMWare, Mooly Sagiv Tel Aviv University

14:00 - 15:30	compilation and optimization 1OOPSLA at Room II

14:00 15m Talk		Back to Direct Style: Typed and Tight OOPSLA Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of Tübingen DOI Pre-print
14:15 15m Talk		Rapid: Region-based Pointer Disambiguation OOPSLA Khushboo Chitre IIIT Delhi, Piyus Kedia IIIT Delhi, Rahul Purandare University of Nebraska-Lincoln
14:30 15m Talk		Automated Ambiguity Detection in Layout-Sensitive Grammars OOPSLA Jiangyi Liu Tsinghua University, Fengmin Zhu CISPA Helmholtz Center for Information Security, Fei He Tsinghua University Pre-print
14:45 15m Talk		Formally Verifying Optimizations with Block Simulations OOPSLA Leo Gourdin Université Grenoble-Alpes, Benjamin Bonneau ENS PSL, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux CNRS/VERIMAG, Alexandre Bérard Université Grenoble-Alpes DOI Pre-print
15:00 15m Talk		Hardware-Aware Static Optimization of Hyperdimensional Computations OOPSLA Pu (Luke) Yi Stanford University, Sara Achour MIT

14:00 - 15:30	security & privacyOOPSLA at Room XII

14:00 18m Talk		Compositional Security Definitions for Higher-Order Where Declassification OOPSLA Jan Menz MPI-SWS, Andrew K. Hirsch University at Buffalo, SUNY, Peixuan Li Pennsylvania State University, Deepak Garg MPI-SWS DOI
14:18 18m Talk		Fat Pointers for Temporal Memory Safety of C OOPSLA Jie Zhou University of Rochester, John Criswell University of Rochester, Michael Hicks Amazon Web Services and the University of Maryland DOI
14:36 18m Talk		Quantifying and Mitigating Cache Side Channel Leakage with Differential Set OOPSLA Cong Ma University of Waterloo, Dinghao Wu , Gang Tan Pennsylvania State University, Mahmut Taylan Kandemir Pennsylvania State University, Danfeng Zhang Duke University, Penn State University
14:54 18m Talk		A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations OOPSLA Anthony C. J. Fox ARM, Gareth Stockwell ARM, Shale Xiong ARM, Hanno Becker Amazon Web Services, Dominic P. Mulligan Amazon Web Services, Gustavo Petri Amazon Web Services, Nathan Chong Amazon Web Services DOI
15:12 18m Talk		Verifying Indistinguishability of Privacy-Preserving Protocols OOPSLA Kirby Linvill University of Colorado Boulder, Gowtham Kaki University of Colorado Boulder, Eric Wustrow University of Colorado Boulder

	15:30 - 16:00	Coffee BreakCatering at I + II foyer

16:00 - 17:30	distribution & networking 2OOPSLA at Room I

16:00 18m Talk		Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection OOPSLA Lorenzo Gheri University of Oxford, 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
16:36 18m Talk		Message Chains for Distributed System Verification OOPSLA Federico Mora University of California, Berkeley, Ankush Desai Amazon Web Services, Elizabeth Polgreen University of Edinburgh, Sanjit A. Seshia University of California, Berkeley
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

16:00 - 17:30	refactoringOOPSLA at Room II

16:00 18m Talk		Aliasing Limits on Translating C to Safe Rust OOPSLA Mehmet Emre University of San Francisco, Peter Boyland University of California at Santa Barbara, Aesha Parekh University of California at Santa Barbara, Ryan Schroeder University of California at Santa Barbara, Kyle Dewey California State University, Ben Hardekopf University of California at Santa Barbara DOI Pre-print
16:18 18m Talk		Adventure of a Lifetime: Extract Method Refactoring for Rust OOPSLA Sewen Thy Ahrefs Research, Andreea Costea School of Computing, National University Of Singapore, Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore DOI Pre-print
16:36 18m Talk		Inductive Program Synthesis Guided by Observational Program Similarity OOPSLA John Feser Massachusetts Institute of Technology, Işil Dillig University of Texas at Austin, Armando Solar-Lezama Massachusetts Institute of Technology
16:54 18m Talk		Automated Translation of Functional Big Data Queries to SQL OOPSLA Guoqiang Zhang North Carolina State University, Benjamin Mariano University of Texas at Austin, Xipeng Shen North Carolina State University, Işil Dillig University of Texas at Austin DOI
17:12 18m Talk		User-Customizable Transpilation of Scripting Languages OOPSLA Bo Wang National University of Singapore, Aashish Kolluri National University of Singapore, Ivica Nikolić National University of Singapore, Teodora Baluta National University of Singapore, Prateek Saxena National University of Singapore DOI

16:00 - 17:30	separation logicOOPSLA at Room XII

16:00 18m Talk		Verification-Preserving Inlining in Automatic Separation Logic Verifiers OOPSLA Thibault Dardinier ETH Zurich, Gaurav Parthasarathy ETH Zurich, Peter Müller ETH Zurich DOI
16:18 18m Talk		Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA Simon Friis Vindum Aarhus University, Lars Birkedal Aarhus University
16:36 18m Talk		Leaf: Modularity for Temporary Sharing in Separation Logic OOPSLA Travis Hance Carnegie Mellon University, Jon Howell VMware Research, Oded Padon VMware Research, Bryan Parno Carnegie Mellon University
16:54 18m Talk		Proof Automation for Linearizability in Separation Logic OOPSLA Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen DOI Pre-print
17:12 18m Talk		Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic OOPSLA Jaehwang Jung KAIST, South Korea, Janggun Lee KAIST, Jaemin Choi , Jaewoo Kim KAIST, Sunho Park KAIST, Jeehoon Kang KAIST

Accepted Papers

	Title
	Accelerating Fuzzing through Prefix-Guided Execution OOPSLA Shaohua Li, Zhendong Su DOI
	A Cocktail Approach to Practical Call Graph Construction OOPSLA Yuandao Cai, Charles Zhang
	A Container-Usage-Pattern-based Context Debloating Approach for Object-Sensitive Pointer Analysis OOPSLA Dongjie He, Yujiang Gui, Wei Li, Yonggang Tao, Changwei Zou, Yulei Sui, Jingling Xue
	A Deductive Verification Infrastructure for Probabilistic Programs OOPSLA Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
	Adventure of a Lifetime: Extract Method Refactoring for Rust OOPSLA Sewen Thy, Andreea Costea, Kiran Gopinathan, Ilya Sergey DOI Pre-print
	A Gradual Probabilistic Lambda Calculus OOPSLA Wenjia Ye, Matías Toro, Federico Olmedo DOI
	A Grounded Conceptual Model for Ownership Types in Rust OOPSLA Will Crichton, Gavin Gray, Shriram Krishnamurthi DOI Pre-print
	Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs OOPSLA Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, Harshit Jitendra Motwani DOI
	Aliasing Limits on Translating C to Safe Rust OOPSLA Mehmet Emre, Peter Boyland, Aesha Parekh, Ryan Schroeder, Kyle Dewey, Ben Hardekopf DOI Pre-print
	An Explanation Method for Models of Code OOPSLA Yu WANG, Ke Wang, Linzhang Wang
	A Pretty Expressive Printer OOPSLA Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak Pre-print
	Asparagus: Automated Synthesis of Parametric Gas Upper-bounds for Smart Contracts OOPSLA Zhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, S. Hitarth
	AST vs. Bytecode: Interpreters in the Age of Meta-Compilation OOPSLA Octave Larose, Sophie Kaleba, Humphrey Burchell, Stefan Marr DOI Pre-print
	AtomiS: Data-centric synchronization made practical OOPSLA Hervé Paulino, Ana Matos, Jan Cederquist, Marco Giunti, João Batista Pereira Matos Júnior, Antonio Ravara
	Automated Ambiguity Detection in Layout-Sensitive Grammars OOPSLA Jiangyi Liu, Fengmin Zhu, Fei He Pre-print
	Automated Translation of Functional Big Data Queries to SQL OOPSLA Guoqiang Zhang, Benjamin Mariano, Xipeng Shen, Işil Dillig DOI
	A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations OOPSLA Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, Nathan Chong DOI
	Back to Direct Style: Typed and Tight OOPSLA Marius Müller, Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann DOI Pre-print
	Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics OOPSLA Girish Mururu, Sharjeel Khan, Bodhisatwa Chatterjee, Chao Chen, Chris Porter, Ada Gavrilovska, Santosh Pande
	Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects OOPSLA Xing Zhang, Guanchen Guo, Xiao He, Zhenjiang Hu DOI
	Bring Your Own Data Structures to Datalog OOPSLA Arash Sahebolamri, Langston Barrett, Scott Moore, Kristopher Micinski
	Building Dynamic System Call Sandbox With Partial Order Analysis OOPSLA Quan Zhang, Chijin Zhou, Yiwen Xu, Zijing Yin, Mingzhe Wang, Zhuo Su, Chengnian Sun, Yu Jiang, Jiaguang Sun
	Compiling Structured Tensor Algebra OOPSLA Mahdi Ghorbani, Mathieu Huot, Shideh Hashemian, Amir Shaikhha
	Complete First-Order Reasoning for Properties of Functional Programs OOPSLA Adithya Murali, Lucas Pena, Ranjit Jhala, P. Madhusudan
	Compositional Security Definitions for Higher-Order Where Declassification OOPSLA Jan Menz, Andrew K. Hirsch, Peixuan Li, Deepak Garg DOI
	Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks OOPSLA Pengfei Gao, Yedi Zhang, Fu Song, Taolue Chen, Francois-Xavier Standaert
	Concrete Type Inference for Code Optimization Using Machine Learning with SMT Solving OOPSLA Fangke Ye, Jisheng Zhao, Jun Shirako, Vivek Sarkar
	Continuing WebAssembly with Effect Handlers OOPSLA Luna Phipps-Costin, Andreas Rossberg, Arjun Guha, Daan Leijen, Daniel Hillerström, KC Sivaramakrishnan, Matija Pretnar, Sam Lindley Pre-print
	Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols OOPSLA Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv
	Data Extraction via Semantic Regular Expression Synthesis OOPSLA Qiaochu Chen, Arko Banerjee, Çağatay Demiralp, Greg Durrett, Işil Dillig
	Deep Learning Robustness Verification for Few-Pixel Attacks OOPSLA Yuval Shapira, Eran Avneri, Dana Drachsler Cohen DOI
	Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions OOPSLA Christopher Wagner, Nouraldin Jaber, Roopsha Samanta DOI
	Equality Saturation Theory Exploration à la Carte OOPSLA Anjali Pal, Brett Saiki, Oliver Flatt, Ryan Tjoa, Amy Zhu, Cynthia Richey, Max Willsey, Zachary Tatlock, Chandrakana Nandi Pre-print
	Exact Recursive Probabilistic Programming OOPSLA David Chiang, Colin McDonald, Chung-chieh Shan DOI
	Explainable Program Synthesis by Localizing Specifications OOPSLA Amirmohammad Nazari, Yifei Huang, Roopsha Samanta, Arjun Radhakrishna, Mukund Raghothaman
	Exploiting the Sparseness of Control-flow and Call Graphs for Efficient and On-demand Algebraic Program Analysis OOPSLA Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Kerim Kochekov, Yun Chen Tsai, Ahmed Khaled Zaher
	Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems OOPSLA Magnus Madsen, Jaco van de Pol, Troels Henriksen
	Fat Pointers for Temporal Memory Safety of C OOPSLA Jie Zhou, John Criswell, Michael Hicks DOI
	Fluent APIs in Functional Languages OOPSLA Ori Roth, Yossi Gil DOI Pre-print
	Formal Abstractions for Packet Scheduling OOPSLA Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, Dexter Kozen
	Formally Verifying Optimizations with Block Simulations OOPSLA Leo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard DOI Pre-print
	From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers OOPSLA Marius Müller, Philipp Schuster, Jonathan Lindegaard Starup, Klaus Ostermann, Jonathan Immanuel Brachthäuser
	Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier OOPSLA Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Roşu DOI
	Getting Into The Flow: Better Type Error Messages for Constraint-Based Type Inference OOPSLA Ishan Bhanuka, Lionel Parreaux, David Binder, Jonathan Immanuel Brachthäuser
	Gradual Typing for Effect Handlers OOPSLA Max New, Eric Giovannini, Dan Licata
	Graph IRs for Impure Higher-Order Languages - Making Aggressive Optimizations Affordable with Precise Effect Dependencies OOPSLA Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, Tiark Rompf
	Greedy Implicit Bounded Quantification OOPSLA Chen Cui, Shengyi Jiang, Bruno C. d. S. Oliveira
	Grounded Copilot: How Programmers Interact with Code-Generating Models OOPSLA Shraddha Barke, Michael B. James, Nadia Polikarpova DOI
	Hardware-Aware Static Optimization of Hyperdimensional Computations OOPSLA Pu (Luke) Yi, Sara Achour
	Historia: Refuting Callback Reachability with Message-History Logics OOPSLA Shawn Meier, Sergio Mover, Gowtham Kaki, Bor-Yuh Evan Chang
	How Domain Experts Use an Embedded DSL OOPSLA Lisa Rennels, Sarah E. Chasins
	How Profilers Can Help Navigate Type Migration OOPSLA Ben Greenman, Matthias Felleisen, Christos Dimoulas
	Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection OOPSLA Lorenzo Gheri, Nobuko Yoshida DOI
	Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection OOPSLA Ruyi Ji, Chaozhe Kong, Yingfei Xiong, Zhenjiang Hu DOI
	Inductive Program Synthesis Guided by Observational Program Similarity OOPSLA John Feser, Işil Dillig, Armando Solar-Lezama
	Inference of Resource Management Specifications OOPSLA Narges Shadab, PRITAM MANOHAR GHARAT, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu K. Lahiri, Akash Lal, Manu Sridharan
	Initializing Global Objects: Time and Order OOPSLA Fengyun Liu, Ondřej Lhoták, David Hua, Enze Xing
	Interactive Debugging of Datalog Programs OOPSLA André Pacak, Sebastian Erdweg
	Languages with Decidable Learning: A Meta-theorem OOPSLA Paul Krogmeier, P. Madhusudan DOI
	Leaf: Modularity for Temporary Sharing in Separation Logic OOPSLA Travis Hance, Jon Howell, Oded Padon, Bryan Parno
	Live Pattern Matching with Typed Holes OOPSLA Yongwei Yuan, Scott Guest, Eric Griffis, Hannah Potter, David Moon, Cyrus Omar DOI
	Lower Bounds for Possibly Divergent Probabilistic Programs OOPSLA Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan DOI
	Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid OOPSLA Huanqi Cao, Shizhi Tang, Qianchao Zhu, Bowen Yu, Wenguang Chen
	Mechanizing Session-Types Using a Structural View: Enforcing linearity without linearity OOPSLA Chuta Sano, Ryan Kavanagh, Brigitte Pientka
	Melocoton: A Program Logic for Verified Interoperability Between OCaml and C OOPSLA Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
	MemPerf: Profiling Allocator-Induced Performance Slowdowns OOPSLA Jin Zhou, Sam Silvestro, Jiaxun,Tang , Hanmei Yang, Hongyu Liu, Guangming Zeng, Bo Wu, Cong Liu, Tongping Liu
	Message Chains for Distributed System Verification OOPSLA Federico Mora, Ankush Desai, Elizabeth Polgreen, Sanjit A. Seshia
	Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates OOPSLA Aalok Thakkar, Nathaniel Sands, Georgios Petrou, Rajeev Alur, Mayur Naik, Mukund Raghothaman
	Modular Component-Based Quantum Circuit Synthesis OOPSLA Chan Gu Kang, Hakjoo Oh DOI
	Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic OOPSLA Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon Kang
	Mutually Iso-recursive Subtyping OOPSLA Andreas Rossberg
	Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning OOPSLA Noam Zilberstein, Derek Dreyer, Alexandra Silva DOI Pre-print
	P4R-Type: a Verified API for P4 Control Plane Programs OOPSLA Roberto Guanciale, Alceste Scalas, Philipp Haller, Jens Kanstrup Larsen DOI Pre-print Media Attached
	Perception Contracts for Safety of ML-Enabled Systems OOPSLA Angello Astorga, Chiao Hsieh, P. Madhusudan, Sayan Mitra
	Proof Automation for Linearizability in Separation Logic OOPSLA Ike Mulder, Robbert Krebbers DOI Pre-print
	Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction OOPSLA Zhenyang Xu, Yongqiang Tian, Mengxiao Zhang, Gaosen Zhao, Yu Jiang, Chengnian Sun DOI
	Quantifying and Mitigating Cache Side Channel Leakage with Differential Set OOPSLA Cong Ma, Dinghao Wu, Gang Tan, Mahmut Taylan Kandemir, Danfeng Zhang
	Randomized Testing of Byzantine Fault Tolerant Algorithms OOPSLA Levin N. Winter, Florena Buse, Daan de Graaf, Klaus von Gleissenthall, Burcu Kulahcioglu Ozkan DOI
	Rapid: Region-based Pointer Disambiguation OOPSLA Khushboo Chitre, Piyus Kedia, Rahul Purandare
	Reference Capabilities for Flexible Memory Management OOPSLA Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew Parkinson, Tobias Wrigstad
	Regular Expression Matching using Bit Vector Automata OOPSLA Alexis Le Glaunec, Lingkun Kong, Konstantinos Mamouras DOI
	Resource-aware soundness for big-step semantics OOPSLA Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca
	Reusing Just-in-Time Compiled Code OOPSLA Meetesh Kalpesh Mehta, Sebastián Krynski, Hugo Musso Gualandi, Manas Thakur, Jan Vitek
	Rhombus: A New Spin on Macros Without All the Parentheses OOPSLA Matthew Flatt, Taylor Allred, Ross Angle, Stephen De Gabrielle, Robby Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, Sam Tobin-Hochstadt Pre-print
	Run-Time Prevention of Software Integration Failures of Machine Learning APIs OOPSLA Chengcheng Wan, Yuhan Liu, Kuntai Du, Henry Hoffmann, Junchen Jiang, Michael Maire, Shan Lu
	Saggitarius: A DSL for Specifying Grammatical Domains OOPSLA Anders Miltner, Devon Loehr, Arnold Mong, Kathleen Fisher, David Walker
	Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data OOPSLA Thierry Renaux, Sam Van den Vonder, Wolfgang De Meuter DOI Pre-print
	Simple Reference Immutability for System F-Sub OOPSLA Edward Lee, Ondřej Lhoták
	Solving Conditional Linear Recurrences for Program Verification: The Periodic Case OOPSLA Chenglin Wang, Fangzhen Lin DOI
	Solving String Constraints with Lengths by Stabilization OOPSLA Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Juraj Síč
	Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA Simon Friis Vindum, Lars Birkedal
	Static Analysis of Memory Models for SMT Encodings OOPSLA Thomas Haas, René Maseli, Roland Meyer, Hernán Ponce de León
	Structural Subtyping as Parametric Polymorphism OOPSLA Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley
	Stuttering for Free OOPSLA Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, Derek Dreyer
	Synthesizing Efficient Memoization Algorithms OOPSLA Yican Sun, Xuanyu Peng, Yingfei Xiong
	Synthesizing Precise Static Analyzers for Automatic Differentiation OOPSLA Jacob Laurel, Siyuan Brant Qian, Gagandeep Singh, Sasa Misailovic
	Synthesizing Specifications OOPSLA Kanghee Park, Loris D'Antoni, Thomas Reps
	TASTyTruffle: Just-in-time Specialization of Parametric Polymorphism OOPSLA Matt D'Souza, James You, Ondřej Lhoták, Aleksandar Prokopec
	The Bounded Pathwidth of Control-flow Graphs OOPSLA Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Chun Kit LAM
	The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog OOPSLA Qinlin Chen, Nairen Zhang, Jinpeng Wang, Tian Tan, Chang Xu, Xiaoxing Ma, Yue Li
	Towards Better Semantics Exploration for Browser Fuzzing OOPSLA Chijin Zhou, Quan Zhang, Lihua Guo, Mingzhe Wang, Yu Jiang, Qing Liao, Zhiyong Wu, Shanshan Li, Bin Gu
	Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs OOPSLA Alex Renda, Yi Ding, Michael Carbin Pre-print
	Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network OOPSLA Shangwen Wang, Bo Lin, Zhensu Sun, Ming Wen, Yepang Liu, Yan Lei, Xiaoguang Mao DOI Pre-print
	Type-Safe Dynamic Placement with First-Class Placed Values OOPSLA George Zakhour, Pascal Weisenburger, Guido Salvaneschi DOI Pre-print
	User-Customizable Transpilation of Scripting Languages OOPSLA Bo Wang, Aashish Kolluri, Ivica Nikolić, Teodora Baluta, Prateek Saxena DOI
	Validating IoT Devices with Rate-Based Session Types OOPSLA Grant Iraci, Cheng-En Chuang, Raymond Hu, Lukasz Ziarek
	Verification-Preserving Inlining in Automatic Separation Logic Verifiers OOPSLA Thibault Dardinier, Gaurav Parthasarathy, Peter Müller DOI
	Verifying Indistinguishability of Privacy-Preserving Protocols OOPSLA Kirby Linvill, Gowtham Kaki, Eric Wustrow
	Verus: Verifying Rust Programs using Linear Ghost Types OOPSLA Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel DOI
	When Concurrency Matters: Behaviour-Oriented Concurrency OOPSLA Luke Cheeseman, Matthew Parkinson, Sylvan Clebsch, Marios Kogias, Sophia Drossopoulou, David Chisnall, Tobias Wrigstad, Paul Liétar

Call for Papers

The OOPSLA issue of the Proceedings of the ACM on Programming Languages (PACMPL) welcomes papers focusing on all practical and theoretical investigations of programming languages, systems and environments. Papers may target any stage of software development, including requirements, modeling, prototyping, design, implementation, generation, analysis, verification, testing, evaluation, maintenance, and reuse of software systems. Contributions may include the development of new tools, techniques, principles, and evaluations.

OOPSLA 2023 will have two separate rounds of reviewing, with Round 1 submission deadline: October 28, 2022 and and Round 2 submission deadline: April 14, 2023
In each round, papers will have a final outcome of Accept, Revise, or Reject—see Review Process for details.

Papers accepted at either of the rounds will be published in the 2023 volume of PACMPL(OOPSLA) and invited to be presented at the SPLASH conference in October 2023.

Review Process

PACMPL(OOPSLA) has two rounds of reviewing. The final outcome of each round can be one of Accept, Revise or Reject.

Accept: Accepted papers will appear in the 2023 volume of PACMPL(OOPSLA).

Revise: Papers in this category are invited to submit a revision to the next round of submissions with a specific set of expectations to be met. When authors resubmit, they should clearly explain how the revisions address the comments of the reviewers, by including a document describing the changes and – if possible – a diff of the PDF as supplementary material. The revised paper will be re-evaluated, and either accepted or rejected. Resubmitted papers will retain the same reviewers throughout the process. Papers with a Revise outcome in Round 2 and an Accept outcome in the subsequent Round 1 will appear in the 2024 volume of PACMPL(OOPSLA).

Reject: Rejected papers will not be included in the 2023 volume of PACMPL(OOPSLA). Papers in this category are not guaranteed a review if resubmitted less than one year from the date of original submission. A paper will be judged to be a resubmission if it is substantially similar to the original submission. The judgment that a paper is a resubmission of the same work and whether, in this case, it will be reviewed or not is at the discretion of the Chair. Obviously, this same policy applies to papers that were rejected for inclusion in the 2022 volume of PACMPL(OOPSLA).

Each round of reviewing consists of two phases. The first phase evaluates the papers and results in an early notification of Reject, Revise, or Conditional Accept. During the first phase, authors will be able to read their reviews and respond to them. The second phase is restricted to conditionally accepted papers. Authors must make a set of mandatory revisions. The second phase assesses whether the required revisions have been addressed. The outcome can be Accept, Revise or Reject.

Submissions

Submitted papers (including resubmissions) must be at most 23 pages using the template below. The references do not count towards this limit. No appendices are allowed on the main paper, instead authors can upload supplementary material with no page or content restrictions, but reviewers may choose to ignore it. The PACMPL templates used for SPLASH (Microsoft Word and LaTeX) can be found at the SIGPLAN author information page. In particular, authors using LaTeX should use the acmart-pacmpl-template.tex file (with the acmsmall option). Papers are expected to use author-year citations. Author-year citations may be used as either a noun phrase, such as “The lambda calculus was originally conceived by Church (1932)”, or a parenthetic phase, such as “The lambda calculus (Church 1932) was intended as a foundation for mathematics”.

PACMPL uses double-blind reviewing. Authors’ identities are only revealed if a paper is accepted. Papers must

omit author names and institutions,
use the third person when referencing your work,
anonymise supplementary material.

Nothing should be done in the name of anonymity that weakens the submission; see the DBR FAQ. When in doubt, contact the Review Committee Chairs.

Papers must describe unpublished work that is not currently submitted for publication elsewhere as described by SIGPLAN’s Republication Policy. Submitters should also be aware of ACM’s Policy and Procedures on Plagiarism. Submissions are expected to comply with the ACM Policies for Authorship.

Artifacts

Authors should indicate with their initial submission if an artifact exists, describe its nature and limitations, and indicate if it will be submitted for evaluation. Accepted papers that fail to provide an artifact will be requested to explain the reason they cannot support replication. It is understood that some papers have no artifacts.

Publication

PACMPL is a Gold Open Access journal, all papers will be freely available to the public. Authors can voluntarily cover the article processing charge ($400), but payment is not required. The official publication date is the date the journal are made available in the ACM Digital Library. The journal issue and associated papers may be published up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work.

FAQ

Selection Criteria

We consider the following criteria when evaluating papers:

Novelty: The paper presents new ideas and results and places them appropriately within the context established by previous research.

Importance: The paper contributes to the advancement of knowledge in the field. We also welcome papers that diverge from the dominant trajectory of the field.

Evidence: The paper presents sufficient evidence supporting its claims, such as proofs, implemented systems, experimental results, statistical analyses, case studies, and anecdotes.

Clarity: The paper presents its contributions, methodology and results clearly.

Artifacts

Q: Are artifacts required?

No! It is understood that some papers have no artifacts. But if an artifact is not provided when the claims in the paper refer to an artifact, the authors must explain why their work is not available for repetition.

Q: Can a paper be accepted if the artifact is rejected?

Yes! The reasons for rejecting an artifact are multiple and often stem from the quality of the packaging.

Double-Blinding Submissions (Authors)

Q: What exactly do I have to do to anonymize my paper?

Use common sense. Your job is not to make your identity undiscoverable but simply to make it possible for reviewers to evaluate your submission without having to know who you are. The specific guidelines stated in the call for papers are simple: omit authors’ names from your title page, and when you cite your own work, refer to it in the third person. For example, if your name is Smith and you have worked on amphibious type systems, instead of saying “We extend our earlier work on statically typed toads [Smith 2004],” you might say “We extend Smith’s [2004] earlier work on statically typed toads.” Also, be sure not to include any acknowledgements that would give away your identity.

Q: Should I change the name of my system?

No.

Q: My submission is based on code available in a public repository. How do I deal with this?

Cite the code in your paper, but remove the URL and, instead say “link to repository removed for double blind review”. If you believe reviewer access to your code would help during author response, contact the Review Committee Chairs.

Q: I am submitting an extension of my workshop paper, should I anonymize reference to that work?

No. But we recommend you do not use the same title, so that it is clearly distinguishes the papers.

Q: Am I allowed to post my paper on my web page or arXiv? send it to colleagues? give a talk about it? on social media?

We have developed guidelines to help navigate the tension between the normal communication of scientific results and actions that essentially force potential reviewers to learn the identity of authors. Roughly speaking, you may discuss work under submission, but you should not broadly advertise your work through media that is likely to reach your reviewers. We acknowledge there are gray areas and trade-offs. Things you may do:

Put your submission on your home page.
Discuss your work with anyone not on the review committees or reviewers with whom you already have a conflict.
Present your work at professional meetings, job interviews, etc.
Submit work previously discussed at an informal workshop, previously posted on arXiv or a similar site, previously submitted to a conference not using double-blind reviewing, etc.

Things you should not do:

Contact members of the review committee about your work, or deliberately present your work where you expect them to be.
Publicize your work on social media if wide public [re-]propagation is common (e.g., Twitter) and therefore likely to reach potential reviewers. For example, on Facebook, a post with a broad privacy setting (public or all friends) saying, “Whew, OOPSLA paper in, time to sleep” is okay, but one describing the work or giving its title is not appropriate. Alternately, a post to a group including only the colleagues at your institution is fine.

Reviewers will not be asked to recuse themselves from reviewing your paper unless they feel you have gone out of your way to advertise your authorship information to them. If you are unsure about what constitutes “going out of your way”, please contact the Review Committee Chairs.

Important dates

2023-04-19 – Quick expertise check.
2023-04-24 – Start of the review phase.
2023-05-08 – 30% of papers due.
2023-05-22 – 60% of papers due.
2023-06-09 – All reviews due.
2023-06-16 – Start of asynchronous discussions (2 weeks).
2023-06-28 + 2023-06-29, 14:00-18:00 UTC – potential sync meetings
2023-06-30 – Author notification.
2023-08-13 – Revision check for conditional accepts (2 weeks).
2023-08-27 – Final author notification.

Assignments: TPMS for initial assignment; you quickly scan assigned papers to judge the expertise and possibly suggest external reviewers; we use the information to reassign papers, if necessary.

Reviews: Please hand in reviews in the batches indicated by the timeline. Discussions after author response will happen mostly asynchronously. Only in case of disagreement will there be a synchronous discussion only for undecided papers.

Cascais

Lisboa

Palácio da Pena

Quinta da Regaleira

Pastel de Belém

Terreiro do Paço

Castelo de São Jorge

Linha de Cascais

Coastal Train Line between Lisbon and Cascais

OOPSLASPLASH 2023

This program is tentative and subject to change.

Program Display Configuration

Wed 25 OctDisplayed time zone: Lisbon change

Thu 26 OctDisplayed time zone: Lisbon change

Fri 27 OctDisplayed time zone: Lisbon change

Accepted Papers

Call for Papers

Information for Reviewers

Mira MeziniPC Chair

TU Darmstadt

Germany

Derek DreyerAssociate Chair

MPI-SWS

Germany

Sophia DrossopoulouAssociate Chair

Imperial College London

United Kingdom

Patrick EugsterAssociate Chair

USI Lugano; Purdue University

Switzerland

Shriram KrishnamurthiAssociate Chair

Brown University, United States

Jonathan Aldrich

Carnegie Mellon University

United States

Karim Ali

University of Alberta

Peter Alvaro

University of California, Santa Cruz

Stephanie Balzer

Carnegie Mellon University

United States

Osbert Bastani

University of Pennsylvania

United States

Annette Bieniusa

University of Kaiserslautern-Landau

Germany

Sebastian Burckhardt

Microsoft Research

United States

Satish Chandra

Meta Platforms

United States

James Cheney

University of Edinburgh

United Kingdom

Pavel Chuprikov

USI Lugano

Switzerland

Albert Cohen

Google

France

Wolfgang De Meuter

Vrije Universiteit Brussel

Belgium

Dominique Devriese

KU Leuven

Belgium

Dana Drachsler Cohen

Technion

Israel

Jana Dunfield

Queen's University, Kingston, Ontario

Canada

Sebastian Erdweg

JGU Mainz

Germany

Matthew Flatt

University of Utah

Wed 25 Oct
Displayed time zone: Lisbon change

Thu 26 Oct
Displayed time zone: Lisbon change

Fri 27 Oct
Displayed time zone: Lisbon change