OOPSLA2 2023
Proceedings of the ACM on Programming Languages, Volume 7, Number OOPSLA2

Title Page

Article: oopslab23foreword-fm000-p doi:

Editorial Message

Article: oopslab23foreword-fm001-p doi:

Hardware-Aware Static Optimization of Hyperdimensional Computations
Pu (Luke) Yi and Sara Achour
(Stanford University, USA)

Publisher's Version Published Artifact Archive submitted (1.3 MB) Artifacts Available Artifacts Functional Article: oopslab23main-p50-p doi:10.1145/3622797

Leaf: Modularity for Temporary Sharing in Separation Logic
Travis Hance, Jon Howell, Oded Padon, and Bryan Parno
(Carnegie Mellon University, USA; VMware Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p53-p doi:10.1145/3622798

Formally Verifying Optimizations with Block Simulations
Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, and Alexandre Bérard
(Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p60-p doi:10.1145/3622799

Synthesizing Efficient Memoization Algorithms
Yican Sun, Xuanyu Peng, and Yingfei Xiong
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p68-p doi:10.1145/3622800

AtomiS: Data-Centric Synchronization Made Practical
Hervé Paulino, Ana Almeida Matos, Jan Cederquist, Marco Giunti, João Matos, and António Ravara
(Nova University of Lisbon, Portugal; University of Lisbon, Portugal)

Publisher's Version Article: oopslab23main-p73-p doi:10.1145/3622801

Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data
Thierry Renaux, Sam Van den Vonder, and Wolfgang De Meuter
(Vrije Universiteit Brussel, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p93-p doi:10.1145/3622802

Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics
Girish Mururu, Sharjeel Khan, Bodhisatwa Chatterjee, Chao Chen, Chris Porter, Ada Gavrilovska, and Santosh Pande
(Georgia Institute of Technology, USA; IBM Research, USA)

Publisher's Version Published Artifact Archive submitted (3.8 MB) Artifacts Available Article: oopslab23main-p95-p doi:10.1145/3622803

Compiling Structured Tensor Algebra
Mahdi Ghorbani, Mathieu Huot, Shideh Hashemian, and Amir Shaikhha
(University of Edinburgh, UK; University of Oxford, UK)

Publisher's Version Artifacts Functional Article: oopslab23main-p99-p doi:10.1145/3622804

The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog
Qinlin Chen, Nairen Zhang, Jinpeng Wang, Tian Tan, Chang Xu, Xiaoxing Ma, and Yue Li
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p118-p doi:10.1145/3622805

Run-Time Prevention of Software Integration Failures of Machine Learning APIs
Chengcheng Wan, Yuhan Liu, Kuntai Du, Henry Hoffmann, Junchen Jiang, Michael Maire, and Shan Lu
(East China Normal University, China; University of Chicago, USA; Microsoft, Redmon, USA)

Publisher's Version Article: oopslab23main-p121-p doi:10.1145/3622806

The Bounded Pathwidth of Control-Flow Graphs
Giovanna Kobus Conrado, Amir Kafshdar Goharshady, and Chun Kit Lam
(Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Published Artifact Artifacts Available Article: oopslab23main-p128-p doi:10.1145/3622807

AST vs. Bytecode: Interpreters in the Age of Meta-Compilation
Octave Larose, Sophie Kaleba, Humphrey Burchell, and Stefan Marr
(University of Kent, UK)

Publisher's Version Published Artifact Archive submitted (360 kB) Artifacts Available Artifacts Reusable Article: oopslab23main-p138-p doi:10.1145/3622808

Mutually Iso-Recursive Subtyping
Andreas Rossberg
(Independent Researcher, Munich, Germany)

Publisher's Version Article: oopslab23main-p150-p doi:10.1145/3622809

Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity
Chuta Sano, Ryan Kavanagh, and Brigitte Pientka
(McGill University, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p177-p doi:10.1145/3622810

Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies
Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Galois, USA; Augusta University, USA)

Publisher's Version Article: oopslab23main-p178-p doi:10.1145/3622813

Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference
Ishan Bhanuka, Lionel Parreaux, David Binder, and Jonathan Immanuel Brachthäuser
(Hong Kong University of Science and Technology, China; University of Tübingen, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p183-p doi:10.1145/3622812

Continuing WebAssembly with Effect Handlers
Luna Phipps-Costin, Andreas Rossberg, Arjun Guha, Daan Leijen, Daniel Hillerström, KC Sivaramakrishnan, Matija Pretnar, and Sam Lindley
(Northeastern University, USA; Independent, Germany; Roblox, USA; Microsoft Research, USA; Huawei Zurich Research Center, Switzerland; Tarides, India; IIT Madras, India; University of Ljubljana, Slovenia; Institute of Mathematics, Physics, and Mechanics, Ljubljana, Slovenia; University of Edinburgh, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p195-p doi:10.1145/3622814

Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network
Shangwen Wang, Bo Lin, Zhensu Sun, Ming Wen, Yepang Liu, Yan Lei, and Xiaoguang Mao
(National University of Defense Technology, China; Singapore Management University, Singapore; Huazhong University of Science and Technology, China; Southern University of Science and Technology, China; Chongqing University, China)

Publisher's Version Published Artifact Artifacts Available Article: oopslab23main-p197-p doi:10.1145/3622815

Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems
Magnus Madsen, Jaco van de Pol, and Troels Henriksen
(Aarhus University, Denmark; University of Copenhagen, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p199-p doi:10.1145/3622816

How Profilers Can Help Navigate Type Migration
Ben Greenman, Matthias Felleisen, and Christos Dimoulas
(University of Utah, USA; Northeastern University, USA; Northwestern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p201-p doi:10.1145/3622817

Rhombus: A New Spin on Macros without All the Parentheses
Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, and Sam Tobin-Hochstadt
(University of Utah, USA; independent, USA; independent, UK; Northwestern University, USA; National University of Singapore, Singapore; Brown University, USA; Reach, USA; University of Washington, USA; independent, Denmark; Indiana University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p205-p doi:10.1145/3622818

Towards Better Semantics Exploration for Browser Fuzzing
Chijin Zhou, Quan Zhang, Lihua Guo, Mingzhe Wang, Yu Jiang, Qing Liao, Zhiyong Wu, Shanshan Li, and Bin Gu
(Tsinghua University, China; Harbin Institute of Technology, China; National University of Defense Technology, China; Beijing Institute of Control Engineering, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p214-p doi:10.1145/3622819

Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
Simon Friis Vindum and Lars Birkedal
(Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p219-p doi:10.1145/3622820

Adventure of a Lifetime: Extract Method Refactoring for Rust
Sewen Thy, Andreea Costea, Kiran Gopinathan, and Ilya Sergey
(Yale-NUS College, Singapore; National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p224-p doi:10.1145/3622821

Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid
Huanqi Cao, Shizhi Tang, Qianchao Zhu, Bowen Yu, and Wenguang Chen
(Tsinghua University, China; Peking University, China; Pengcheng Laboratory, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p227-p doi:10.1145/3622822

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, and Derek Dreyer
(Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, France; Saarland University, Germany; MPI-SWS, Germany; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p230-p doi:10.1145/3622823

Interactive Debugging of Datalog Programs
André Pacak and Sebastian Erdweg
(JGU Mainz, Germany)

Publisher's Version Article: oopslab23main-p232-p doi:10.1145/3622824

Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving
Fangke Ye, Jisheng Zhao, Jun Shirako, and Vivek Sarkar
(Georgia Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Article: oopslab23main-p242-p doi:10.1145/3622825

An Explanation Method for Models of Code
Yu Wang, Ke Wang, and Linzhang Wang
(Nanjing University, China; Visa Research, USA)

Publisher's Version Archive submitted (570 kB) Article: oopslab23main-p245-p doi:10.1145/3622826

Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, and Jeehoon Kang
(KAIST, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p248-p doi:10.1145/3622827

Simple Reference Immutability for System F_<:
Edward Lee and Ondřej Lhoták
(University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p249-p doi:10.1145/3622828

Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts
Zhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, and S. Hitarth
(Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p265-p doi:10.1145/3622829

Inductive Program Synthesis Guided by Observational Program Similarity
Jack Feser, Işıl Dillig, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA; University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p275-p doi:10.1145/3622830

From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers
Marius Müller, Philipp Schuster, Jonathan Lindegaard Starup, Klaus Ostermann, and Jonathan Immanuel Brachthäuser
(University of Tübingen, Germany; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p278-p doi:10.1145/3622831

A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis
Dongjie He, Yujiang Gui, Wei Li, Yonggang Tao, Changwei Zou, Yulei Sui, and Jingling Xue
(UNSW, Australia)

Publisher's Version Article: oopslab23main-p282-p doi:10.1145/3622832

A Cocktail Approach to Practical Call Graph Construction
Yuandao Cai and Charles Zhang
(Hong Kong University of Science and Technology, China)

Publisher's Version Article: oopslab23main-p284-p doi:10.1145/3622833

Equality Saturation Theory Exploration à la Carte
Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, and Chandrakana Nandi
(University of Washington, USA; Certora, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p292-p doi:10.1145/3622834

Complete First-Order Reasoning for Properties of Functional Programs
Adithya Murali, Lucas Peña, Ranjit Jhala, and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA; University of California at San Diego, USA)

Publisher's Version Article: oopslab23main-p305-p doi:10.1145/3622835

Structural Subtyping as Parametric Polymorphism
Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, and Sam Lindley
(University of Edinburgh, UK; Huawei Zurich Research Center, Switzerland; Heriot-Watt University, UK; TU Berlin, Germany; University of Glasgow, UK)

Publisher's Version Archive submitted (1.1 MB) Article: oopslab23main-p306-p doi:10.1145/3622836

A Pretty Expressive Printer
Sorawee Porncharoenwase, Justin Pombrio, and Emina Torlak
(University of Washington, USA; Unaffiliated, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p307-p doi:10.1145/3622837

Automated Ambiguity Detection in Layout-Sensitive Grammars
Jiangyi Liu, Fengmin Zhu, and Fei He
(Tsinghua University, China; CISPA Helmholtz Center for Information Security, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p314-p doi:10.1145/3622838

Reusing Just-in-Time Compiled Code
Meetesh Kalpesh Mehta, Sebastián Krynski, Hugo Musso Gualandi, Manas Thakur, and Jan Vitek
(IIT Mandi, India; Czech Technical University in Prague, Czechia; IIT Bombay, India; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p315-p doi:10.1145/3622839

Bring Your Own Data Structures to Datalog
Arash Sahebolamri, Langston Barrett, Scott Moore, and Kristopher Micinski
(Syracuse University, USA; Galois, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p329-p doi:10.1145/3622840

A Grounded Conceptual Model for Ownership Types in Rust
Will Crichton, Gavin Gray, and Shriram Krishnamurthi
(Brown University, USA; ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p335-p doi:10.1145/3622841

Building Dynamic System Call Sandbox with Partial Order Analysis
Quan Zhang, Chijin Zhou, Yiwen Xu, Zijing Yin, Mingzhe Wang, Zhuo Su, Chengnian Sun, Yu Jiang, and Jiaguang Sun
(Tsinghua University, China; University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p352-p doi:10.1145/3622842

Resource-Aware Soundness for Big-Step Semantics
Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca
(University of Genoa, Italy; University of Eastern Piedmont, Italy)

Publisher's Version Article: oopslab23main-p371-p doi:10.1145/3622843

Initializing Global Objects: Time and Order
Fengyun Liu, Ondřej Lhoták, David Hua, and Enze Xing
(Oracle Labs, Switzerland; University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p374-p doi:10.1145/3622844

Formal Abstractions for Packet Scheduling
Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, and Dexter Kozen
(Cornell University, USA; Open University of the Netherlands, Netherlands; University of Amsterdam, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p376-p doi:10.1145/3622845

Reference Capabilities for Flexible Memory Management
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, and Tobias Wrigstad
(Uppsala University, Sweden; Microsoft Azure Research, USA; Imperial College London, UK; Research & Programming, New Zealand; Microsoft Azure Research, UK)

Publisher's Version Article: oopslab23main-p377-p doi:10.1145/3622846

Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates
Aalok Thakkar, Nathaniel Sands, George Petrou, Rajeev Alur, Mayur Naik, and Mukund Raghothaman
(University of Pennsylvania, USA; University of Southern California, USA)

Publisher's Version Article: oopslab23main-p386-p doi:10.1145/3622847

MemPerf: Profiling Allocator-Induced Performance Slowdowns
Jin Zhou, Sam Silvestro, Steven (Jiaxun) Tang, Hanmei Yang, Hongyu Liu, Guangming Zeng, Bo Wu, Cong Liu, and Tongping Liu
(University of Massachusetts at Amherst, USA; University of Texas at San Antonio, USA; Synopsys, USA; Colorado School of Mines, USA; University of Texas at Dallas, USA)

Publisher's Version Article: oopslab23main-p395-p doi:10.1145/3622848

Verifying Indistinguishability of Privacy-Preserving Protocols
Kirby Linvill, Gowtham Kaki, and Eric Wustrow
(University of Colorado Boulder, USA)

Publisher's Version Article: oopslab23main-p404-p doi:10.1145/3622849

Quantifying and Mitigating Cache Side Channel Leakage with Differential Set
Cong Ma, Dinghao Wu, Gang Tan, Mahmut Taylan Kandemir, and Danfeng Zhang
(University of Waterloo, Canada; Pennsylvania State University, USA; Duke University, USA)

Publisher's Version Published Artifact Artifacts Available Article: oopslab23main-p409-p doi:10.1145/3622850

How Domain Experts Use an Embedded DSL
Lisa Rennels and Sarah E. Chasins
(University of California at Berkeley, USA)

Publisher's Version Article: oopslab23main-p415-p doi:10.1145/3622851

When Concurrency Matters: Behaviour-Oriented Concurrency
Luke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias, Sophia Drossopoulou, David Chisnall, Tobias Wrigstad, and Paul Liétar
(Imperial College London, UK; Microsoft Azure Research, UK; Microsoft Research, UK; Microsoft, UK; Uppsala University, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p418-p doi:10.1145/3622852

TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism
Matt D'Souza, James You, Ondřej Lhoták, and Aleksandar Prokopec
(University of Waterloo, Canada; Oracle Labs, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p432-p doi:10.1145/3622853

Validating IoT Devices with Rate-Based Session Types
Grant Iraci, Cheng-En Chuang, Raymond Hu, and Lukasz Ziarek
(University at Buffalo, USA; Queen Mary University of London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p437-p doi:10.1145/3622854

Static Analysis of Memory Models for SMT Encodings
Thomas Haas, René Maseli, Roland Meyer, and Hernán Ponce de León
(TU Braunschweig, Germany; Huawei, Germany)

Publisher's Version Published Artifact Archive submitted (530 kB) Artifacts Available Artifacts Functional Article: oopslab23main-p447-p doi:10.1145/3622855

Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs
Alex Renda, Yi Ding, and Michael Carbin
(Massachusetts Institute of Technology, USA; Purdue University, USA)

Publisher's Version Published Artifact Archive submitted (4.1 MB) Artifacts Available Article: oopslab23main-p463-p doi:10.1145/3622856

Stuttering for Free
Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, and Derek Dreyer
(Seoul National University, Republic of Korea; MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p465-p doi:10.1145/3622857

Inference of Resource Management Specifications
Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu K. Lahiri, Akash Lal, and Manu Sridharan
(University of California at Riverside, USA; Microsoft Research, India; University of Washington, USA; New Jersey Institute of Technology, USA; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p471-p doi:10.1145/3622858

Rapid: Region-Based Pointer Disambiguation
Khushboo Chitre, Piyus Kedia, and Rahul Purandare
(IIIT Delhi, India; University of Nebraska-Lincoln, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p475-p doi:10.1145/3622859

Gradual Typing for Effect Handlers
Max S. New, Eric Giovannini, and Daniel R. Licata
(University of Michigan, USA; Wesleyan University, USA)

Publisher's Version Article: oopslab23main-p476-p doi:10.1145/3622860

Synthesizing Specifications
Kanghee Park, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p481-p doi:10.1145/3622861

Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks
Pengfei Gao, Yedi Zhang, Fu Song, Taolue Chen, and Francois-Xavier Standaert
(ShanghaiTech University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; University of London, UK; Université Catholique de Louvain, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p513-p doi:10.1145/3622862

Data Extraction via Semantic Regular Expression Synthesis
Qiaochu Chen, Arko Banerjee, Çağatay Demiralp, Greg Durrett, and Işıl Dillig
(University of Texas at Austin, USA; Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p524-p doi:10.1145/3622863

Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols
Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, and Mooly Sagiv
(Tel Aviv University, Israel; University of Texas at Austin, USA; VMware Research, USA; VMware Research, Israel)

Publisher's Version Article: oopslab23main-p541-p doi:10.1145/3622864

Historia: Refuting Callback Reachability with Message-History Logics
Shawn Meier, Sergio Mover, Gowtham Kaki, and Bor-Yuh Evan Chang
(University of Colorado Boulder, USA; École Polytechnique - CNRS - Institut Polytechnique de Paris, France; Amazon, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p556-p doi:10.1145/3622865

P4R-Type: A Verified API for P4 Control Plane Programs
Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller, and Alceste Scalas
(DTU, Denmark; KTH Royal Institute of Technology, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p569-p doi:10.1145/3622866

Synthesizing Precise Static Analyzers for Automatic Differentiation
Jacob Laurel, Siyuan Brant Qian, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; Zhejiang University, China; VMware Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p573-p doi:10.1145/3622867

Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis
Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Kerim Kochekov, Yun Chen Tsai, and Ahmed Khaled Zaher
(Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslab23main-p586-p doi:10.1145/3622868

Saggitarius: A DSL for Specifying Grammatical Domains
Anders Miltner, Devon Loehr, Arnold Mong, Kathleen Fisher, and David Walker
(Simon Fraser University, Canada; Princeton University, USA; Tufts University, USA)

Publisher's Version Article: oopslab23main-p640-p doi:10.1145/3622869

A Deductive Verification Infrastructure for Probabilistic Programs
Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p651-p doi:10.1145/3622870

Greedy Implicit Bounded Quantification
Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p664-p doi:10.1145/3622871

Solving String Constraints with Lengths by Stabilization
Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč
(Academia Sinica, Taiwan; Brno University of Technology, Czechia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p692-p doi:10.1145/3622872

Type-Safe Dynamic Placement with First-Class Placed Values
George Zakhour, Pascal Weisenburger, and Guido Salvaneschi
(University of St. Gallen, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslab23main-p706-p doi:10.1145/3622873

Explainable Program Synthesis by Localizing Specifications
Amirmohammad Nazari, Yifei Huang, Roopsha Samanta, Arjun Radhakrishna, and Mukund Raghothaman
(University of Southern California, USA; Purdue University, USA; Microsoft, USA)

Publisher's Version Published Artifact Archive submitted (430 kB) Artifacts Available Artifacts Reusable Article: oopslab23main-p769-p doi:10.1145/3622874

Perception Contracts for Safety of ML-Enabled Systems
Angello Astorga, Chiao Hsieh, P. Madhusudan, and Sayan Mitra
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version Article: oopslab23main-p773-p doi:10.1145/3622875

Message Chains for Distributed System Verification
Federico Mora, Ankush Desai, Elizabeth Polgreen, and Sanjit A. Seshia
(University of California at Berkeley, USA; Amazon Web Services, USA; University of Edinburgh, UK)

Publisher's Version Article: oopslab23main-p782-p doi:10.1145/3622876