OOPSLA2 2023
Proceedings of the ACM on Programming Languages, Volume 7, Number OOPSLA2
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 7, Number OOPSLA2, October 22–27, 2023, Cascais, Portugal

OOPSLAB – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message

Papers

Hardware-Aware Static Optimization of Hyperdimensional Computations
Pu (Luke) Yi ORCID logo and Sara Achour ORCID logo
(Stanford University, USA)
Publisher's Version Published Artifact Archive submitted (1.3 MB) Artifacts Available Artifacts Functional
Leaf: Modularity for Temporary Sharing in Separation Logic
Travis Hance ORCID logo, Jon Howell ORCID logo, Oded Padon ORCID logo, and Bryan ParnoORCID logo
(Carnegie Mellon University, USA; VMware Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Formally Verifying Optimizations with Block Simulations
Léo Gourdin ORCID logo, Benjamin Bonneau ORCID logo, Sylvain BoulméORCID logo, David MonniauxORCID logo, and Alexandre Bérard ORCID logo
(Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, France)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Synthesizing Efficient Memoization Algorithms
Yican Sun ORCID logo, Xuanyu Peng ORCID logo, and Yingfei Xiong ORCID logo
(Peking University, China)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
AtomiS: Data-Centric Synchronization Made Practical
Hervé Paulino ORCID logo, Ana Almeida Matos ORCID logo, Jan Cederquist ORCID logo, Marco Giunti ORCID logo, João Matos ORCID logo, and António Ravara ORCID logo
(Nova University of Lisbon, Portugal; University of Lisbon, Portugal)
Publisher's Version
Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data
Thierry Renaux ORCID logo, Sam Van den Vonder ORCID logo, and Wolfgang De Meuter ORCID logo
(Vrije Universiteit Brussel, Belgium)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics
Girish Mururu ORCID logo, Sharjeel Khan ORCID logo, Bodhisatwa ChatterjeeORCID logo, Chao Chen ORCID logo, Chris Porter ORCID logo, Ada Gavrilovska ORCID logo, and Santosh Pande ORCID logo
(Georgia Institute of Technology, USA; IBM Research, USA)
Publisher's Version Published Artifact Archive submitted (3.8 MB) Artifacts Available
Compiling Structured Tensor Algebra
Mahdi Ghorbani ORCID logo, Mathieu Huot ORCID logo, Shideh Hashemian ORCID logo, and Amir Shaikhha ORCID logo
(University of Edinburgh, UK; University of Oxford, UK)
Publisher's Version Artifacts Functional
The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog
Qinlin Chen ORCID logo, Nairen Zhang ORCID logo, Jinpeng Wang ORCID logo, Tian Tan ORCID logo, Chang XuORCID logo, Xiaoxing Ma ORCID logo, and Yue Li ORCID logo
(Nanjing University, China)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Run-Time Prevention of Software Integration Failures of Machine Learning APIs
Chengcheng WanORCID logo, Yuhan Liu ORCID logo, Kuntai Du ORCID logo, Henry HoffmannORCID logo, Junchen Jiang ORCID logo, Michael Maire ORCID logo, and Shan LuORCID logo
(East China Normal University, China; University of Chicago, USA; Microsoft, Redmon, USA)
Publisher's Version
The Bounded Pathwidth of Control-Flow Graphs
Giovanna Kobus Conrado ORCID logo, Amir Kafshdar Goharshady ORCID logo, and Chun Kit Lam ORCID logo
(Hong Kong University of Science and Technology, Hong Kong)
Publisher's Version Published Artifact Artifacts Available
AST vs. Bytecode: Interpreters in the Age of Meta-Compilation
Octave Larose ORCID logo, Sophie Kaleba ORCID logo, Humphrey Burchell ORCID logo, and Stefan Marr ORCID logo
(University of Kent, UK)
Publisher's Version Published Artifact Archive submitted (360 kB) Artifacts Available Artifacts Reusable
Mutually Iso-Recursive Subtyping
Andreas RossbergORCID logo
(Independent Researcher, Munich, Germany)
Publisher's Version
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity
Chuta Sano ORCID logo, Ryan Kavanagh ORCID logo, and Brigitte PientkaORCID logo
(McGill University, Canada)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies
Oliver Bračevac ORCID logo, Guannan Wei ORCID logo, Songlin Jia ORCID logo, Supun Abeysinghe ORCID logo, Yuxuan Jiang ORCID logo, Yuyan Bao ORCID logo, and Tiark Rompf ORCID logo
(Purdue University, USA; Galois, USA; Augusta University, USA)
Publisher's Version
Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference
Ishan Bhanuka ORCID logo, Lionel Parreaux ORCID logo, David BinderORCID logo, and Jonathan Immanuel Brachthäuser ORCID logo
(Hong Kong University of Science and Technology, China; University of Tübingen, Germany)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Continuing WebAssembly with Effect Handlers
Luna Phipps-Costin ORCID logo, Andreas RossbergORCID logo, Arjun Guha ORCID logo, Daan LeijenORCID logo, Daniel HillerströmORCID logo, KC SivaramakrishnanORCID logo, Matija Pretnar ORCID logo, and Sam Lindley ORCID logo
(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
Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network
Shangwen WangORCID logo, Bo Lin ORCID logo, Zhensu Sun ORCID logo, Ming WenORCID logo, Yepang Liu ORCID logo, Yan Lei ORCID logo, and Xiaoguang Mao ORCID logo
(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
Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems
Magnus Madsen ORCID logo, Jaco van de Pol ORCID logo, and Troels Henriksen ORCID logo
(Aarhus University, Denmark; University of Copenhagen, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
How Profilers Can Help Navigate Type Migration
Ben Greenman ORCID logo, Matthias Felleisen ORCID logo, and Christos Dimoulas ORCID logo
(University of Utah, USA; Northeastern University, USA; Northwestern University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Rhombus: A New Spin on Macros without All the Parentheses
Matthew Flatt ORCID logo, Taylor Allred ORCID logo, Nia Angle ORCID logo, Stephen De Gabrielle ORCID logo, Robert Bruce Findler ORCID logo, Jack Firth ORCID logo, Kiran GopinathanORCID logo, Ben Greenman ORCID logo, Siddhartha Kasivajhula ORCID logo, Alex Knauth ORCID logo, Jay McCarthy ORCID logo, Sam Phillips ORCID logo, Sorawee Porncharoenwase ORCID logo, Jens Axel Søgaard ORCID logo, and Sam Tobin-Hochstadt ORCID logo
(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
Towards Better Semantics Exploration for Browser Fuzzing
Chijin Zhou ORCID logo, Quan Zhang ORCID logo, Lihua Guo ORCID logo, Mingzhe Wang ORCID logo, Yu JiangORCID logo, Qing Liao ORCID logo, Zhiyong Wu ORCID logo, Shanshan Li ORCID logo, and Bin Gu ORCID logo
(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
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
Simon Friis VindumORCID logo and Lars BirkedalORCID logo
(Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Adventure of a Lifetime: Extract Method Refactoring for Rust
Sewen Thy ORCID logo, Andreea Costea ORCID logo, Kiran GopinathanORCID logo, and Ilya SergeyORCID logo
(Yale-NUS College, Singapore; National University of Singapore, Singapore)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid
Huanqi Cao ORCID logo, Shizhi Tang ORCID logo, Qianchao Zhu ORCID logo, Bowen Yu ORCID logo, and Wenguang Chen ORCID logo
(Tsinghua University, China; Peking University, China; Pengcheng Laboratory, China)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
Armaël GuéneauORCID logo, Johannes Hostert ORCID logo, Simon Spies ORCID logo, Michael Sammler ORCID logo, Lars BirkedalORCID logo, and Derek DreyerORCID logo
(Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, France; Saarland University, Germany; MPI-SWS, Germany; Aarhus University, Denmark)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Interactive Debugging of Datalog Programs
André Pacak ORCID logo and Sebastian ErdwegORCID logo
(JGU Mainz, Germany)
Publisher's Version
Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving
Fangke Ye ORCID logo, Jisheng Zhao ORCID logo, Jun Shirako ORCID logo, and Vivek Sarkar ORCID logo
(Georgia Institute of Technology, USA)
Publisher's Version Published Artifact Artifacts Available
An Explanation Method for Models of Code
Yu Wang ORCID logo, Ke Wang ORCID logo, and Linzhang Wang ORCID logo
(Nanjing University, China; Visa Research, USA)
Publisher's Version Archive submitted (570 kB)
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
Jaehwang Jung ORCID logo, Janggun Lee ORCID logo, Jaemin Choi ORCID logo, Jaewoo Kim ORCID logo, Sunho Park ORCID logo, and Jeehoon KangORCID logo
(KAIST, Republic of Korea)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Simple Reference Immutability for System F<:
Edward Lee ORCID logo and Ondřej Lhoták ORCID logo
(University of Waterloo, Canada)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts
Zhuo Cai ORCID logo, Soroush Farokhnia ORCID logo, Amir Kafshdar Goharshady ORCID logo, and S. Hitarth ORCID logo
(Hong Kong University of Science and Technology, Hong Kong)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Inductive Program Synthesis Guided by Observational Program Similarity
Jack FeserORCID logo, Işıl Dillig ORCID logo, and Armando Solar-Lezama ORCID logo
(Massachusetts Institute of Technology, USA; University of Texas at Austin, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers
Marius Müller ORCID logo, Philipp Schuster ORCID logo, Jonathan Lindegaard Starup ORCID logo, Klaus Ostermann ORCID logo, and Jonathan Immanuel Brachthäuser ORCID logo
(University of Tübingen, Germany; Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis
Dongjie He ORCID logo, Yujiang Gui ORCID logo, Wei Li ORCID logo, Yonggang Tao ORCID logo, Changwei Zou ORCID logo, Yulei Sui ORCID logo, and Jingling Xue ORCID logo
(UNSW, Australia)
Publisher's Version
A Cocktail Approach to Practical Call Graph Construction
Yuandao Cai ORCID logo and Charles ZhangORCID logo
(Hong Kong University of Science and Technology, China)
Publisher's Version
Equality Saturation Theory Exploration à la Carte
Anjali Pal ORCID logo, Brett Saiki ORCID logo, Ryan Tjoa ORCID logo, Cynthia Richey ORCID logo, Amy Zhu ORCID logo, Oliver Flatt ORCID logo, Max WillseyORCID logo, Zachary Tatlock ORCID logo, and Chandrakana NandiORCID logo
(University of Washington, USA; Certora, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Complete First-Order Reasoning for Properties of Functional Programs
Adithya MuraliORCID logo, Lucas Peña ORCID logo, Ranjit JhalaORCID logo, and P. MadhusudanORCID logo
(University of Illinois at Urbana-Champaign, USA; University of California at San Diego, USA)
Publisher's Version
Structural Subtyping as Parametric Polymorphism
Wenhao TangORCID logo, Daniel HillerströmORCID logo, James McKinna ORCID logo, Michel Steuwer ORCID logo, Ornela DardhaORCID logo, Rongxiao Fu ORCID logo, and Sam Lindley ORCID logo
(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)
A Pretty Expressive Printer
Sorawee Porncharoenwase ORCID logo, Justin Pombrio ORCID logo, and Emina Torlak ORCID logo
(University of Washington, USA; Unaffiliated, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Automated Ambiguity Detection in Layout-Sensitive Grammars
Jiangyi Liu ORCID logo, Fengmin ZhuORCID logo, and Fei HeORCID logo
(Tsinghua University, China; CISPA Helmholtz Center for Information Security, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Reusing Just-in-Time Compiled Code
Meetesh Kalpesh Mehta ORCID logo, Sebastián Krynski ORCID logo, Hugo Musso Gualandi ORCID logo, Manas Thakur ORCID logo, and Jan Vitek ORCID logo
(IIT Mandi, India; Czech Technical University in Prague, Czechia; IIT Bombay, India; Northeastern University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Bring Your Own Data Structures to Datalog
Arash Sahebolamri ORCID logo, Langston Barrett ORCID logo, Scott Moore ORCID logo, and Kristopher Micinski ORCID logo
(Syracuse University, USA; Galois, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
A Grounded Conceptual Model for Ownership Types in Rust
Will Crichton ORCID logo, Gavin Gray ORCID logo, and Shriram Krishnamurthi ORCID logo
(Brown University, USA; ETH Zurich, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Building Dynamic System Call Sandbox with Partial Order Analysis
Quan Zhang ORCID logo, Chijin Zhou ORCID logo, Yiwen Xu ORCID logo, Zijing Yin ORCID logo, Mingzhe Wang ORCID logo, Zhuo Su ORCID logo, Chengnian Sun ORCID logo, Yu JiangORCID logo, and Jiaguang Sun ORCID logo
(Tsinghua University, China; University of Waterloo, Canada)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Resource-Aware Soundness for Big-Step Semantics
Riccardo Bianchini ORCID logo, Francesco Dagnino ORCID logo, Paola Giannini ORCID logo, and Elena ZuccaORCID logo
(University of Genoa, Italy; University of Eastern Piedmont, Italy)
Publisher's Version
Initializing Global Objects: Time and Order
Fengyun Liu ORCID logo, Ondřej Lhoták ORCID logo, David Hua ORCID logo, and Enze Xing ORCID logo
(Oracle Labs, Switzerland; University of Waterloo, Canada)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Formal Abstractions for Packet Scheduling
Anshuman Mohan ORCID logo, Yunhe Liu ORCID logo, Nate FosterORCID logo, Tobias KappéORCID logo, and Dexter KozenORCID logo
(Cornell University, USA; Open University of the Netherlands, Netherlands; University of Amsterdam, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Reference Capabilities for Flexible Memory Management
Ellen Arvidsson ORCID logo, Elias Castegren ORCID logo, Sylvan Clebsch ORCID logo, Sophia Drossopoulou ORCID logo, James NobleORCID logo, Matthew J. Parkinson ORCID logo, and Tobias Wrigstad ORCID logo
(Uppsala University, Sweden; Microsoft Azure Research, USA; Imperial College London, UK; Research & Programming, New Zealand; Microsoft Azure Research, UK)
Publisher's Version
Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates
Aalok Thakkar ORCID logo, Nathaniel Sands ORCID logo, George Petrou ORCID logo, Rajeev AlurORCID logo, Mayur Naik ORCID logo, and Mukund Raghothaman ORCID logo
(University of Pennsylvania, USA; University of Southern California, USA)
Publisher's Version
MemPerf: Profiling Allocator-Induced Performance Slowdowns
Jin Zhou ORCID logo, Sam Silvestro ORCID logo, Steven (Jiaxun) Tang ORCID logo, Hanmei Yang ORCID logo, Hongyu Liu ORCID logo, Guangming Zeng ORCID logo, Bo Wu ORCID logo, Cong Liu ORCID logo, and Tongping Liu ORCID logo
(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
Verifying Indistinguishability of Privacy-Preserving Protocols
Kirby Linvill ORCID logo, Gowtham KakiORCID logo, and Eric Wustrow ORCID logo
(University of Colorado Boulder, USA)
Publisher's Version
Quantifying and Mitigating Cache Side Channel Leakage with Differential Set
Cong Ma ORCID logo, Dinghao Wu ORCID logo, Gang TanORCID logo, Mahmut Taylan Kandemir ORCID logo, and Danfeng Zhang ORCID logo
(University of Waterloo, Canada; Pennsylvania State University, USA; Duke University, USA)
Publisher's Version Published Artifact Artifacts Available
How Domain Experts Use an Embedded DSL
Lisa RennelsORCID logo and Sarah E. ChasinsORCID logo
(University of California at Berkeley, USA)
Publisher's Version
When Concurrency Matters: Behaviour-Oriented Concurrency
Luke Cheeseman ORCID logo, Matthew J. Parkinson ORCID logo, Sylvan Clebsch ORCID logo, Marios Kogias ORCID logo, Sophia Drossopoulou ORCID logo, David Chisnall ORCID logo, Tobias Wrigstad ORCID logo, and Paul Liétar ORCID logo
(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
TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism
Matt D'Souza ORCID logo, James You ORCID logo, Ondřej Lhoták ORCID logo, and Aleksandar Prokopec ORCID logo
(University of Waterloo, Canada; Oracle Labs, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Validating IoT Devices with Rate-Based Session Types
Grant Iraci ORCID logo, Cheng-En Chuang ORCID logo, Raymond HuORCID logo, and Lukasz Ziarek ORCID logo
(University at Buffalo, USA; Queen Mary University of London, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Static Analysis of Memory Models for SMT Encodings
Thomas Haas ORCID logo, René Maseli ORCID logo, Roland Meyer ORCID logo, and Hernán Ponce de León ORCID logo
(TU Braunschweig, Germany; Huawei, Germany)
Publisher's Version Published Artifact Archive submitted (530 kB) Artifacts Available Artifacts Functional
Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs
Alex RendaORCID logo, Yi Ding ORCID logo, and Michael CarbinORCID logo
(Massachusetts Institute of Technology, USA; Purdue University, USA)
Publisher's Version Published Artifact Archive submitted (4.1 MB) Artifacts Available
Stuttering for Free
Minki Cho ORCID logo, Youngju Song ORCID logo, Dongjae Lee ORCID logo, Lennard Gäher ORCID logo, and Derek DreyerORCID logo
(Seoul National University, Republic of Korea; MPI-SWS, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Inference of Resource Management Specifications
Narges Shadab ORCID logo, Pritam Gharat ORCID logo, Shrey Tiwari ORCID logo, Michael D. ErnstORCID logo, Martin Kellogg ORCID logo, Shuvendu K. LahiriORCID logo, Akash LalORCID logo, and Manu Sridharan ORCID logo
(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
Rapid: Region-Based Pointer Disambiguation
Khushboo Chitre ORCID logo, Piyus Kedia ORCID logo, and Rahul Purandare ORCID logo
(IIIT Delhi, India; University of Nebraska-Lincoln, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Gradual Typing for Effect Handlers
Max S. New ORCID logo, Eric Giovannini ORCID logo, and Daniel R. Licata ORCID logo
(University of Michigan, USA; Wesleyan University, USA)
Publisher's Version
Synthesizing Specifications
Kanghee Park ORCID logo, Loris D'AntoniORCID logo, and Thomas RepsORCID logo
(University of Wisconsin-Madison, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks
Pengfei Gao ORCID logo, Yedi Zhang ORCID logo, Fu Song ORCID logo, Taolue Chen ORCID logo, and Francois-Xavier Standaert ORCID logo
(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 Info Artifacts Available Artifacts Functional
Data Extraction via Semantic Regular Expression Synthesis
Qiaochu Chen ORCID logo, Arko Banerjee ORCID logo, Çağatay Demiralp ORCID logo, Greg Durrett ORCID logo, and Işıl Dillig ORCID logo
(University of Texas at Austin, USA; Massachusetts Institute of Technology, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols
Orr Tamir ORCID logo, Marcelo Taube ORCID logo, Kenneth L. McMillan ORCID logo, Sharon Shoham ORCID logo, Jon Howell ORCID logo, Guy Gueta ORCID logo, and Mooly Sagiv ORCID logo
(Tel Aviv University, Israel; University of Texas at Austin, USA; VMware Research, USA; VMware Research, Israel)
Publisher's Version
Historia: Refuting Callback Reachability with Message-History Logics
Shawn Meier ORCID logo, Sergio Mover ORCID logo, Gowtham KakiORCID logo, and Bor-Yuh Evan ChangORCID logo
(University of Colorado Boulder, USA; École Polytechnique - CNRS - Institut Polytechnique de Paris, France; Amazon, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
P4R-Type: A Verified API for P4 Control Plane Programs
Jens Kanstrup Larsen ORCID logo, Roberto Guanciale ORCID logo, Philipp Haller ORCID logo, and Alceste Scalas ORCID logo
(DTU, Denmark; KTH Royal Institute of Technology, Sweden)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Synthesizing Precise Static Analyzers for Automatic Differentiation
Jacob Laurel ORCID logo, Siyuan Brant QianORCID logo, Gagandeep SinghORCID logo, and Sasa MisailovicORCID logo
(University of Illinois at Urbana-Champaign, USA; Zhejiang University, China; VMware Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis
Giovanna Kobus Conrado ORCID logo, Amir Kafshdar Goharshady ORCID logo, Kerim Kochekov ORCID logo, Yun Chen Tsai ORCID logo, and Ahmed Khaled Zaher ORCID logo
(Hong Kong University of Science and Technology, Hong Kong)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Saggitarius: A DSL for Specifying Grammatical Domains
Anders Miltner ORCID logo, Devon Loehr ORCID logo, Arnold Mong ORCID logo, Kathleen Fisher ORCID logo, and David Walker ORCID logo
(Simon Fraser University, Canada; Princeton University, USA; Tufts University, USA)
Publisher's Version
A Deductive Verification Infrastructure for Probabilistic Programs
Philipp Schröer ORCID logo, Kevin Batz ORCID logo, Benjamin Lucien Kaminski ORCID logo, Joost-Pieter Katoen ORCID logo, and Christoph Matheja ORCID logo
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Greedy Implicit Bounded Quantification
Chen Cui ORCID logo, Shengyi Jiang ORCID logo, and Bruno C. d. S. OliveiraORCID logo
(University of Hong Kong, China)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Solving String Constraints with Lengths by Stabilization
Yu-Fang Chen ORCID logo, David Chocholatý ORCID logo, Vojtěch HavlenaORCID logo, Lukáš HolíkORCID logo, Ondřej LengálORCID logo, and Juraj SíčORCID logo
(Academia Sinica, Taiwan; Brno University of Technology, Czechia)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Type-Safe Dynamic Placement with First-Class Placed Values
George Zakhour ORCID logo, Pascal Weisenburger ORCID logo, and Guido Salvaneschi ORCID logo
(University of St. Gallen, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Explainable Program Synthesis by Localizing Specifications
Amirmohammad Nazari ORCID logo, Yifei Huang ORCID logo, Roopsha Samanta ORCID logo, Arjun Radhakrishna ORCID logo, and Mukund Raghothaman ORCID logo
(University of Southern California, USA; Purdue University, USA; Microsoft, USA)
Publisher's Version Published Artifact Archive submitted (430 kB) Artifacts Available Artifacts Reusable
Perception Contracts for Safety of ML-Enabled Systems
Angello AstorgaORCID logo, Chiao Hsieh ORCID logo, P. MadhusudanORCID logo, and Sayan Mitra ORCID logo
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Message Chains for Distributed System Verification
Federico Mora ORCID logo, Ankush Desai ORCID logo, Elizabeth Polgreen ORCID logo, and Sanjit A. Seshia ORCID logo
(University of California at Berkeley, USA; Amazon Web Services, USA; University of Edinburgh, UK)
Publisher's Version

proc time: 11.48