OOPSLA 2021
2021-10-17..2021-10-22
-- online --
OOPSLA ·
[OOPSLA 2018, OOPSLA 2020, OOPSLA 2021, OOPSLA 2022, OOPSLA 2023, OOPSLA 2024, OOPSLA 2025]
as the organisers put it
PACMPL Issue OOPSLA 2021 seeks contributions on all aspects of programming languages and software engineering. Authors of papers published in PACMPL Issue OOPSLA 2021 will be invited to present their work in the OOPSLA track of the SPLASH conference in November. 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 (such as language front-ends, program analyses, and r ...
| title | author | length |
|---|---|---|
| Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation | Artem Pelenitsyn, Julia Belyakova, Benjamin W Chung, Ross Tate, Jan Vitek | 13m |
Formalizes type stability and introduces a stronger property, type groundedness, proves grounded instances always fully devirtualize under a modeled JIT, and… | ||
| Permchecker: A Toolchain for Debugging Memory Managers with Typestate | Karl Cronburg | 15m |
Permchecker makes heap structure explicit by generating a DSL compiler for typestate specs, an LLVM annotation pass, and a PIN dynamic tool that enforces… | ||
| The Reads-From Equivalence for the TSO and PSO Memory Models | Truc Lam Bui, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, Viktor Toman | 14m |
Presents algorithms that decide reads-from (RF) consistency for TSO and PSO with explicit complexity: n^{k+1} bound for TSO and n^{k+1}·min(n^{k^2},2^{k·d})… | ||
| Specifying and Testing GPU Workgroup Progress Models | Tyler Sorensen, Lucas Fernan Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, Alastair F. Donaldson | 15m |
A toolbox formalizes a tiny concurrent language, implements executable semantics in the CDP model checker, synthesizes 483 litmus tests, compiles them to… | ||
| Well-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers | Stefanos Chaliasos, Thodoris Sotiropoulos, Georgios-Petros Drosos, Charalambos Ioannis Mitropoulos, Dimitris Mitropoulos, Diomidis Spinellis | 15m |
Manual analysis of 320 typing-related bugs from Java, Scala, Kotlin and Groovy reveals concrete testing targets and failure modes: more than half are… | ||
| Generative Type-Aware Mutation for Testing SMT Solvers | Jiwon Park, Dominik Winterer, Chengyu Zhang, Zhendong Su | 12m |
Generative Type-Aware Mutation implements expression mutation using SMT-LIB operator signatures to produce grammatically correct but larger mutants, realized… | ||
| Transitioning from Structural to Nominal Code with Efficient Gradual Typing | Fabian Muehlboeck, Ross Tate | 14m |
MonNom is an object language that lets untyped structural records and lambdas dynamically acquire nominal interfaces (but not classes) via monotonic casts… | ||
| A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs | Paul He, Edwin Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic | 13m |
A memory-safe Rust-like type system called Heapster typechecks LLVM IR and extracts Coq functions that represent imperative behavior without pointer reasoning… | ||
| Programming and Execution Models for Parallel Bounded Exhaustive Testing | Nader Al Awar, Kush Jain, Chris Rossbach, Milos Gligoric | 15m |
Tempo presents a concrete system for parallel bounded-exhaustive testing: a small API (explore, choice, ignore), OpenMP CPU and CUDA GPU backends, and three… | ||
| Interpretable Noninterference Measurement and its Application to Processor Designs | Ziqiao Zhou, Michael K. Reiter | 15m |
DINoMe scales quantitative noninterference measurement to a full RISC-V BOOM Verilog core by translating Verilog to SMT2 with Yosys-to-SMT2, composing… | ||
| Fully Automated Functional Fuzzing of Android Apps for Detecting Non-Crashing Logic Bugs | Ting Su, Zhendong Su, Yichen Yan, Jingling Sun, Yiheng Xiong | 13m |
Proposes independent view fuzzing and a tool called Genie that automatically mines a GUI transitional model, finds independent event traces, injects them into… | ||
| SimTyper: Sound Type Inference for Ruby using Type Equality Prediction | Milod Kazerounian, Jeffrey S. Foster, Bonan Min | 14m |
SimTyper infers usable Ruby types by combining constraint solving, InferDL-style heuristics, and a learned type equality prediction model. It builds DeepSim (a… | ||
| Safer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust | Natalie Popescu, Ziyang Xu, Sotiris Apostolakis, David I. August, Amit Levy | 15m |
Rust libraries use unchecked indexing in 10% of the 500 most downloaded packages, and small compiler or workload changes make bounds-check overhead vary… | ||
| Generalizable Synthesis Through Unification | Ruyi Ji, Jingtao Xia, Yingfei Xiong, Zhenjiang Hu | 14m |
Defines an Occam solver with PAC-style guarantees and proves Eusolver fails that criterion, then builds PolyGen, an Occam STUN solver that decomposes CLIA… | ||
| Gradually Structured Data | Stefan Malewski, Michael Greenberg, Éric Tanter | 13m |
A formal core language for “gradually structured data” introduces open and closed algebraic datatypes, two new runtime types—unknown datatype and unknown open… | ||
| Making Pointer Analysis More Precise by Unleashing the Power of Selective Context Sensitivity | Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, Yannis Smaragdakis | 15m |
Proposes Unity-Relay, a meta-framework that combines multiple selective context sensitivity strategies and, when needed, runs them in successive passes using… | ||
| Coarsening Optimization for Differentiable Programming | Xipeng Shen, Guoqiang Zhang, Irene Dea, Samantha Andow, Emilio Arroyo-Fang, Neal Gafter, Johann George, Melissa Grueter, Erik Meijer, Olin Shivers, Steffi Stumpos, Alanna Tempest, Christy Warden, Shannon Yang | 15m |
Paper presents coarsening optimization that raises segments to symbolic level, applies differentiation and lowers optimized code, and reports several-times to… | ||
| Efficient Compilation of Algebraic Effect Handlers | Georgios Karachalias, Filip Koprivec, Matija Pretnar, Tom Schrijvers | 15m |
An optimizing Eff→OCaml compiler is implemented that uses a two-phase ExEff/NoEff pipeline with type-and-effect directed rewrites, function specialization and… | ||
| LXM: Better Splittable Pseudorandom Number Generators (and Almost as Fast) | Guy L. Steele Jr., Sebastiano Vigna | 15m |
LXM is a concrete PRNG design that sums an LCG and an F2-linear (xoroshiro/xoshiro) generator and then applies a mixer, claiming LCG+XBG+mix yields long… | ||
| Not So Fast: Understanding and Mitigating Negative Impacts of Compiler Optimizations on Code Reuse G | Michael D. Brown, Matthew Pruett, Robert Bigelow, Girish Mururu, Santosh Pande | 15m |
Study compares 1,187 variants of 20 benchmarks compiled with GCC and Clang using the gadget analyzer GSA, and finds compiler optimizations massively change… | ||
| Reconciling Optimization With Secure Compilation | Son Tuan Vu, Albert Cohen, Arnaud de Grandmaison, Christophe Guillon, Karine Heydemann | 16m |
Claims a way to make compiler optimizations preserve security-relevant intermediate state by adding opaque observations and an opacification mechanism that… | ||
| Scalability and Precision by Combining Expressive Type Systems and Deductive Verification | Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, Werner Dietl | 14m |
Implementation builds a Property Checker and a JML translator that converts unproven type checks into assertions for KeY/OpenJML and proven ones into… | ||
| Relational Nullable Types with Boolean Unification | Magnus Madsen, Jaco van de Pol | 14m |
Proposes a concrete type system that records two Boolean formulas per expression to track may-null and may-present, extends Hindley‑Milner with Boolean… | ||
| MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels | Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, Akash Lal | 14m |
MonkeyDB is a mock storage that computes, from an axiomatic isolation spec, the full set of values a read could legally return and returns a random value from… | ||
| QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems | Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, Roopsha Samanta | 15m |
QuickSilver introduces the Mercury modeling language with two concrete agreement primitives, Partition and Consensus, that abstract verified Paxos/Raft-style… | ||
| Semantic programming by example with pre-trained models | Gust Verbruggen, Vu Le, Sumit Gulwani | 15m |
A system combines FlashFill-style deductive synthesis with GPT-3 to handle semantic string ops by adding three semantic operators (e.g. SemMap, SemPos) and a… | ||
| Solver-based Gradual Type Migration | Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, Arjun Guha | 12m |
TypeWhich automates gradual type migration by emitting GTLC constraints solved with an off‑the‑shelf MaxSMT-based constraints backend instead of custom… | ||
| Static Detection of Silent Misconfigurations with Deep Interaction Analysis | Jialu Zhang, Ruzica Piskac, Ennan Zhai, Tianyin Xu | 15m |
Builds a tool called ConfigX that statically links configuration entries to code via LLVM IR, applies customized data- and control-flow tainting to derive… | ||
| Synthesizing Contracts Correct Modulo a Test Generator | Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan, Tao Xie | 14m |
Approach synthesizes tight contracts as decision trees and integrates a SyGuS-based learner (CVC4Sy) with the Pex test generator to get guarantees modulo a… | ||
| A Multiparty Session Typing Discipline for Fault-tolerant Event-driven Distributed Programming | Malte Viering, Raymond Hu, Patrick Eugster, Lukasz Ziarek | 15m |
Presents a new MPST formulation that supports event-driven multiparty sessions with handlers for I/O and partial failures, including dynamic replacement of… | ||
| Statically Bounded-Memory Delayed Sampling for Probabilistic Streams | Eric Atkinson, Guillaume Baudart, Louis Mandel, Charles Yuan, Michael Carbin | 15m |
Defines two dataflow conditions, m-consumed and unseparated path, and proves they are necessary and sufficient for delayed sampling to use bounded memory on… | ||
| Making Weak Memory Models Fair | Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis | 14m |
Proposes a uniform memory fairness condition for declarative weak memory models (requires porf-acyclicity) and proves it is equivalent to natural operational… | ||
| Study of the Subtyping Machine of Nominal Subtyping with Variance | Ori Roth | 14m |
Class fragments of Kennedy and Pierce’s nominal subtyping map to concrete tree-language classes: the lattice of fragments is characterized as non-expansive =… | ||
| Label Dependent Lambda Calculus and Gradual Typing | Weili Fu, Fabian Krause, Peter Thiemann | 15m |
A small dependently typed core called the label-dependent lambda calculus models records as functions over first-class labels and adds lightweight… | ||
| APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in Libraries | Xiang Gao, Arjun Radhakrishna, Gustavo Soares, Ridwan Salihin Shariffdeen, Sumit Gulwani, Abhik Roychoudhury | 15m |
APIFix uses output-oriented synthesis to infer API-adaptation edits by mining human edits plus existing updated-library usages, then performs provenance… | ||
| VESPA: Static Profiling for Binary Optimization | Angelica Aparecida Moreira, Guilherme Ottoni, Fernando Magno Quintão Pereira | 14m |
Claims a static profiler that replaces runtime counters in BOLT and produces measurable speedups by predicting branch probabilities via a regression DNN from… | ||
| FPL: Fast Presburger Arithmetic through Transprecision | Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, Tobias Grosser | 14m |
A new C++ Presburger library lives inside MLIR and targets real polyhedral workloads: a benchmark of over 1,000,000 extracted Presburger cases shows… | ||
| Translating C to Safer Rust | Mehmet Emre, Ryan Schroeder, Kyle Dewey, Ben Hardekopf | 15m |
Paper presents an automated C→Rust translation that infers lifetimes and ownership, rewrites function and struct signatures, and iteratively uses Rust compiler… | ||
| Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D | Wolf Honore, Jieung Kim, Ji-Yong Shin, Zhong Shao | 15m |
Presents a fault-aware ADO model that exposes partial failures (uncommitted but visible updates) while hiding protocol internals, and a verification stack… | ||
| Compiling with Continuations, Correctly | Zoe Paraskevopoulou, Anvay Grover | 15m |
Presents a novel simulation that combines syntactic simulations with a logical relation: it uses an untyped step-indexed logical relation parameterized by a… | ||
| Durable Functions: Semantics for Stateful Serverless | Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, Christopher S. Meiklejohn | 15m |
Durable Functions extends FaaS with actors, workflows and entities and claims to give strong, fault free semantics while running on ephemeral workers and… | ||
| Program Analysis via Efficient Symbolic Abstraction | Peisen Yao, Qingkai Shi, Heqing Huang, Charles Zhang | 13m |
Two algorithms compute most-precise abstractions for quantifier-free bit-vector formulas over the interval and a convex polyhedral-like domain, using… | ||
| Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations | Didier Ishimwe, KimHao Nguyen, ThanhVu Nguyen | 15m |
Dynaplex instruments recursive programs, infers recurrences from traces (sizes, recursion depth, loop counts), fits cost terms by regression, and solves with… | ||
| Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts | Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Konstantinos Triantafyllou, Ilias Tsatiris | 15m |
A static analysis combines a Datalog fixpoint engine with a tightly integrated symbolic solver, invoking the solver tens to hundreds of thousands of times to… | ||
| Multi-modal Program Inference: a Marriage of Pre-trained Language Models and Component-based Synthes | Kia Rahmani, Mohammad Raza, Sumit Gulwani, Vu Le, Daniel Morris, Arjun Radhakrishna, Gustavo Soares, Ashish Tiwari | 16m |
NLX combines GPT-3 candidates with a component-based synthesizer to turn ambiguous English plus examples into precise code. It targets regexes and CSS… | ||
| Promises Are Made to be Broken | Aviral Goel, Jan Ječmen, Sebastián Krynski, Olivier Flückiger, Jan Vitek | 14m |
Presents a concrete migration: a dynamic analyzer called LazR that generates strictness signatures for R functions (52K functions, 204K parameters inferred)… | ||
| Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches | Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang | 14m |
Synbit synthesizes well behaved bidirectional programs in HOBiT from a unidirectional get plus a few I/O examples by converting get into a partial sketch… | ||
| Data-Driven Abductive Inference of Library Specifications | Zhe Zhou, Robert F. Dickerson, Benjamin Delaware, Suresh Jagannathan | 15m |
Tool named Elrond infers specifications for black‑box OCaml libraries by combining random testing, SMT counterexample-guided refinement, and an abduction loop… | ||
| The Semantics of Shared Memory in Intel CPU/FPGA Systems | Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, John Wickerson | 13m |
Defines precise weak‑memory behaviors for Intel Xeon + Arria FPGA systems, encoding them as an operational model in CBMC and an axiomatic model in Alloy and… | ||
| JavaDL: Automatically Incrementalizing Java Bug Pattern Detection | Alexandru Dura, Christoph Reichenbach, Emma Söderberg | 12m |
JavaDL is a Datalog-based language that merges fact extraction with analysis so AST nodes are first-class facts and rules use syntactic patterns and semantic… | ||
| Compacting Points-To Sets Through Object Clustering | Mohamad Barbar, Yulei Sui | 15m |
Maps memory objects to integers so bit-vector points-to sets shrink; formulates an optimal mapping as an integer linear program but falls back to fast… | ||
| A Derivative-based Parser Generator for Visibly Pushdown Grammars | Xiaodong Jia, Ashish Kumar, Gang Tan | 14m |
A derivative-based parser generator converts visibly pushdown grammars to a deterministic PDA and produces a shared parse forest in linear time, with a… | ||
| What we Eval in the Shadows | Aviral Goel, Pierre Donat-Bouillud, Filip Krikava, Christoph Kirsch, Jan Vitek | 14m |
Study of 240,327 R scripts (15,401 packages) records 49,296,059 eval calls and exercises ~18k eval call-sites, showing eval is pervasive and varied. Only 6% of… | ||
| SpecSafe: Detecting Cache Side Channels in a Speculative World | Robert Brotzman-Smith, Danfeng Zhang, Mahmut Taylan Kandemir, Gang Tan | 15m |
SpecSafe detects cache side channels by defining Speculative-Aware noninterference (SANI), applying a program transformation that encodes speculative traces so… | ||
| Automatic Migration from Synchronous to Asynchronous JavaScript APIs | Satyajit Gokhale, Alexi Turcotte, Frank Tip | 15m |
A static-analysis refactoring converts synchronous I/O to async/await where safe, implemented as Desynchronizer and applied automatically to 12 projects with… | ||
| Rewrite Rule Inference Using Equality Saturation | Chandrakana Nandi, Max Willsey, Amy Zhu, Brett Saiki, Yisu Remy Wang, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock | 14m |
Describes a system called Ruler that uses equality saturation over e-graphs to infer rewrite rules automatically, implemented in Rust on the egg library… | ||
| Efficient Automatic Scheduling of Imaging & Vision Pipelines for the GPU | Luke Anderson, Andrew Adams, Karima Ma, Tzu-Mao Li, Tian Jin, Jonathan Ragan-Kelley | 15m |
An autoscheduler generates GPU code from Halide algorithm code by combining a two-phase search that freezes low-cost stages, hierarchical sampling that groups… | ||
| One Down, 699 to Go: or, synthesising compositional desugarings | Sándor Bartha, James Cheney, Vaishak Belle | 14m |
Paper claims that decomposing desugaring into an incremental desugaring extension problem plus an extensible hypothesis space makes brute-force synthesis… | ||
| ECROs: Building Global Scale Systems from Sequential Code | Kevin De Porre, Carla Ferreira, Nuno Preguiça, Elisa Gonzalez Boix | 15m |
ECROs derive correct hybrid replicated data types from a sequential Scala implementation plus a distributed specification, with the static analyzer Ordana… | ||
| LooPy: Interactive Program Synthesis with Control Structures | Kasra Ferdowsifard, Shraddha Barke, Hila Peleg, Sorin Lerner, Nadia Polikarpova | 14m |
A Live Programming–integrated synthesizer called LooPy extends Small-Step Live PBE to handle loops by treating holes as runtime pauses and asking the… | ||
| Copy-and-Patch Compilation | Haoran Xu, Fredrik Kjolstad | 15m |
Copy-and-patch compiles by copying prebuilt binary stencils into memory and patching relocations and constants at runtime, shifting heavy work to build time. A… | ||
| Verifying Concurrent Multicopy Search Structures | Nisarg Patel, Siddharth Krishna, Dennis Shasha, Thomas Wies | 14m |
Proves that multicopy search structures satisfy linearizability by isolating a search recency property and a template for upsert/search/maintenance that works… | ||
| Compilation of Sparse Array Programming Models | Rawn Henry, Olivia Hsu, Rohan Yadav, Stephen Chou, Kunle Olukotun, Saman Amarasinghe, Fredrik Kjolstad | 15m |
A compiler built on TACO generates C-like code from array index notation and a format language that supports arbitrary fill values, lifts operators into an… | ||
| Modular Specification and Verification of Closures in Rust | Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, Alexander J. Summers | 15m |
A Prusti extension encodes higher-order Rust closures into first-order Viper logic and discharges verification conditions to Z3, claiming modular verification… | ||
| UDF to SQL Translation through Compositional Lazy Inductive Synthesis | Guoqiang Zhang, Yuanchao Xu, Xipeng Shen, Isil Dillig | 14m |
A tool called CLIS implements compositional lazy inductive synthesis to convert Scala UDFs into pure SQL by building a data‑flow graph, applying DFG… | ||
| SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency | Pengbo Yan, Toby Murray | 14m |
SecRSL is a separation logic that proves information-flow security for C11’s Release-Acquire fragment under an axiomatic memory model and is mechanized in Coq… | ||
| Rich Specifications for Ethereum Smart Contract Verification | Christian Braem, Marco Eilers, Peter Müller, Robin Sierra, Alexander J. Summers | 14m |
Defines a specification style that proves concrete guarantees: sound reasoning under arbitrary re-entrancy, modular verification of collaborating contracts… | ||
| Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs | Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, Tiark Rompf | 15m |
New type system lambda assigns reachability qualifiers to expressions to track exact alias sets, enforces separation for higher-order functions with function… | ||
| Formal Verification of High-Level Synthesis | Yann Herklotz, James Pollard, Nadesh Ramanathan, John Wickerson | 15m |
Presents a mechanically verified HLS tool called Vericert that extends CompCert and is proved correct in Coq, translating CompCert 3AC into an HTL FSM and then… | ||
| Gauss: Program Synthesis by Reasoning Over Graphs | Rohan Bavishi, Caroline Lemieux, Koushik Sen, Ion Stoica | 15m |
Gauss synthesizes table-transformation programs (Pandas and R) from partial outputs plus user intent graphs that record cell/row/column relations (example… | ||
| nothing matches | ||