OOPSLA 2018
2018-11-07..2018-11-09
Boston, United States
OOPSLA ·
[OOPSLA 2018, OOPSLA 2020, OOPSLA 2021, OOPSLA 2022, OOPSLA 2023, OOPSLA 2024, OOPSLA 2025]
as the organisers put it
PACMPL (OOPSLA) seeks contributions on all aspects of programming languages and software engineering. Authors of papers published in PACMPL will present their work at OOPSLA in Boston. 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 runtime systems), new techniques (such as methodologies, design processes, and ...
| title | author | length |
|---|---|---|
| What happens-after the first race? enhancing the predictive power of dynamic race detection | Umang Mathur | 21m |
Proposes schedulable happens-before (SHB), a partial order that exactly characterizes which HB-unordered conflicting accesses are actually schedulable races… | ||
| Virtual Machine Design for Parallel Dynamic Programming Languages | Remigius Meier | 23m |
Claims a concrete VM design: implements parallel worlds for isolation, on-demand page sharing and reconciliation using x86 virtual memory segmentation and… | ||
| Verified Three-Way Program Merge | Marcelo Sousa | 24m |
Claims a verifiable definition of semantic conflict freedom and a Java prototype called SafeMerge that uses a four-way AST diff to produce a shared program… | ||
| Towards Understanding the Costs of Avoiding Out-of-Thin-Air Results | Peizhao Ou | 24m |
Paper implements two concrete fixes in LLVM and measures cost on ARMv8 Cortex‑A72 hardware. One enforces load/store ordering for atomics by adding fences or… | ||
| Thread-Safe Reactive Programming | Joscha Drechsler | 24m |
Claims a runtime scheduler that provides abort-free strict serializability for reactive programs by combining conservative two-phase locking, multi-version… | ||
| The Root Cause of Blame - Contracts for Intersection and Union Types | Jack Williams | 21m |
Extends the untyped lambda calculus with a uniform single reduction rule for monitoring higher-order intersection and union contracts and tags each contract… | ||
| Test Generation for Higher-Order Functions in Dynamic Languages | Marija Selakovic | 21m |
LambdaTester automatically infers which argument positions expect callbacks, synthesizes callbacks with four strategies (including CB-writes that mutates… | ||
| Speeding up Symbolic Reasoning for Relational Queries | Chenglong Wang | 15m |
Presents a space refinement algorithm that soundly shrinks the set of candidate input tables by backward-propagating provenance from a symbolic output… | ||
| Sound Deadlock Prediction | Christian Gram Kalhauge | 19m |
Claims a first sound deadlock predictor for Java that models prediction as a decidable SMT-backed decision problem and actually builds it: a recorder Wiretap… | ||
| Software Multiplexing - Share Your Libraries and Statically Link Them Too | Will Dietz | 25m |
Software Multiplexing compiles programs and their shared libraries into a single static executable using bitcode and a multicall dispatch, implemented in the… | ||
| ShareJIT - JIT Code Cache Sharing across Processes and its Practical Implementation | Xiaoran Xu | 22m |
Builds a global shared JIT cache inside Android Runtime (ART) using a file-backed shared memory region and a global share map keyed by a hash of… | ||
| Scopes as Types | Hendrik van Antwerpen | 27m |
Scope graphs model name binding and the paper’s main claim is that treating scopes as types lets one encode structural and generic type internals uniformly. A… | ||
| Safe Replication through Bounded Concurrency Verification | Gowtham Kaki | 25m |
Automatic bounded verification explores executions under an unrestricted consistency model but with a finite concurrency bound and discovers concrete… | ||
| Robust Relational Layout Synthesis from Examples for Android | Pavol Bielik | 23m |
An end-to-end system called InferUI synthesizes Android relational layouts by encoding 26 ConstraintLayout relations as SMT formulas, adding formal robustness… | ||
| Relational Program Synthesis | Xinyu Wang | 23m |
Defines relational program synthesis and builds Relish, a CEGIS-style tool that combines a compositional relational version space learner with SyGuS… | ||
| Refinement in object-sensitivity points-to analysis via slicing | Raghavan Komondoor | 25m |
Paper: https://dl.acm.org/citation.cfm?id=3276512
Object sensitivity analysis is a well-known form of context-sensitive points-to analysis. This analysis is… | ||
| Reconciling High-level Optimizations and Low-level Code in LLVM | Juneyoung Lee | 22m |
Defines a formal LLVM-IR memory model that uses full provenance and twin allocation to reconcile aggressive high-level memory optimizations with real low-level… | ||
| Reasoning about Security of Amazon Web Services | Byron Cook | 01h 02m |
Amazon Web Services adopts formal verification across design and operation, proving distributed key protocols and TLS code, and using Zelkova to check IAM… | ||
| Reactive Caching for Composed Services | Sebastian Burckhardt | 25m |
Reactive caching maintains summaries and caches with bi-directional links to track dependencies and incrementally repair distributed read-only operations… | ||
| Randomized Testing of Distributed Systems with Probabilistic Guarantees | Burcu Kulahcioglu Ozkan | 23m |
A randomized scheduler called PC-TCP constructs an online chain partition of the observed partial order and samples schedules so that for width w and n events… | ||
| RacerD - Compositional Static Race Detection | Sam Blackshear | 24m |
RacerD is a compositional static race detector that builds compositional interprocedural summaries of syntactic accesses and uses ownership and thread domains… | ||
| Precision-Guided Context Sensitivity for Pointer Analysis | Tian Tan | 26m |
Identifies where context sensitivity matters by spotting direct, rep and unwrap flows that cause objects from different callers to merge, encodes them in a… | ||
| Precise and Scalable Points-to Analysis via Data-Driven Context Tunneling | Minseok Jeon | 17m |
Presents a concrete method called context tunneling that selectively preserves “important” context elements instead of the most-recent k, implemented in the… | ||
| Persistence Semantics for Weak Memory | Azalea Raad | 23m |
Introduces PTSO: an integration of epoch persistency with x86/SPARC TSO that gives both operational and declarative semantics and a machine-checked proof of… | ||
| Parallelization of Dynamic Languages - Synchronizing Built-in Collections | Arie Tal | 23m |
An implementation in TruffleRuby adds a local vs shared heap tag and applies gradual synchronization to Ruby Array and Hash instances, switching from no locks… | ||
| One tool, many languages: language-parametric transformation with incremental parametric syntax | James Koppel | 24m |
A new representation called incremental parametric syntax lets one write a single source-to-source transformation and run it on many real languages with little… | ||
| Object-Oriented Recovery for Non-Volatile Memory | Nachshon Cohen | 19m |
NVMReconstruction implements a Clang/LLVM extension plus runtime library that reconstructs persistent C++ objects after restart by zeroing transient fields… | ||
| Distributed Abstractions | Barbara Liskov | 59m |
Describes Mastry’s tree and the Silo database built on it: in-memory key/value storage using a compare-and-swap header with lock bit and version per node… | ||
| Leto - Verifying Application-Specific Fault Tolerance through Parameterized Execution Models | Brett Boston | 23m |
Leto is an SMT-based verifier that lets developers encode hardware fault semantics and prove relational properties between a fault-free and a relaxed… | ||
| Julia Subtyping - a Rational Reconstruction | Francesco Zappa Nardelli | 20m |
Provides a precise formal definition of Julia’s subtype relation plus a reference implementation that logs and replays actual runtime subtype queries… | ||
| Julia - Dynamism and Performance Reconciled by Design | Benjamin W Chung | 22m |
Julia claims dynamic features plus C-like speed and shows it on benchmarks where most programs run within 2x of C while two outliers are explained by boxing… | ||
| In Defense of "Little Code" | Kathi Fisler | 01h 04m |
Study of the classic rainfall sentinel study finds students taught a design-first, functional approach favor clean-first solutions and show much lower error… | ||
| Incrementalizing Lattice-Based Program Analyses in Datalog | Tamás Szabó | 23m |
Presents DRedL, an algorithm that incrementalizes recursive lattice-value aggregation in Datalog and integrates it into the IncA framework, enabling… | ||
| Identifying Refactoring Opportunities for Replacing Type Code with Subclass and State | Jyothi Vedurada | 21m |
Paper: https://dl.acm.org/citation.cfm?id=3276508
Refactoring is a program transformation that restructures existing code without altering its behaviour and… | ||
| Horn-ICE Learning for Synthesizing Invariants and Contracts | Daniel Neider | 22m |
Algorithm extends ICE to Horn-ICE and claims it synthesizes inductive invariants and contracts for recursive and concurrent code by learning decision trees… | ||
| GraphIt - A High-Performance Graph DSL | Yunming Zhang | 23m |
DSL that separates algorithm from schedule and a scheduling language that composes push/pull direction, partitioning for cache, parallelization, NUMA and… | ||
| Optimal Stateless Model Checking under the Release-Acquire Semantics | Tuan Phong Ngo | 22m |
Claims a provably optimal stateless model checking method for the Release-Acquire fragment of C/C++11 that explores each program order and read‑from relation… | ||
| Finding Broken Promises in Asynchronous JavaScript Programs | Saba Alimadadi | 24m |
PromiseKeeper instruments Node.js programs to build extended promise graphs that model ES6 features (default reactions, exceptions, race/all) via dynamic… | ||
| ExceLint - Automatically Finding Spreadsheet Formula Errors | Daniel W. Barowy | 22m |
ExceLint is a Microsoft Excel plugin that implements a static analysis for spreadsheet formula errors, partitioning sheets into rectangular regions and… | ||
| Every Data Structure Deserves Lock-Free Memory Reclamation | Nachshon Cohen | 21m |
Presents a fully lock-free memory-reclamation system that combines a lock-free mark-and-sweep base with a lightweight, generic root-gathering mechanism applied… | ||
| Empowering Union and Intersection Types with Integrated Subtyping | Fabian Muehlboeck | 22m |
Framework implements a decision procedure that combines a simple, textbook reductive subtyping kernel with user-specified extensions to recognize… | ||
| Effect Handlers for the Masses | Jonathan Immanuel Brachthäuser | 24m |
First Java implementation of algebraic effect handlers: a library plus a bytecode toolchain that performs a type-selective CPS bytecode transform (preserves… | ||
| Distributed System Development with ScalaLoci | Pascal Weisenburger | 23m |
ScalaLoci provides placement types and event streams that encode where values and streams live, generate remote-access code, and statically check… | ||
| DeepBugs - A Learning Approach to Name-based Bug Detection | Michael Pradel | 25m |
Uses simple code transformations to seed millions of training examples, learns identifier embeddings with word2vec and concatenates those vectors into a… | ||
| Gradual Liquid Type Inference | Niki Vazou | 24m |
Combines Liquid Haskell’s liquid refinement type inference with gradual refinement types to solve two problems: global, non-modular inference that needs… | ||
| goSLP - Globally Optimized Superword Level Parallelism Framework | Charith Mendis | 21m |
goSLP formulates SLP statement packing as an ILP solver optimization across whole functions, then solves vector permutation selection with dynamic programming… | ||
| Format Abstraction for Sparse Tensor Algebra Compilers | Stephen Chou | 25m |
Paper demonstrates an abstraction that expresses tensor formats as composable per-dimension level formats and a plugin-style code generator that emits concrete… | ||
| FlashProfile - A Framework for Synthesizing Data Profiles | Saswat Padhi | 21m |
A framework called FlashProfile uses the PROSE inductive-synthesis engine (PROSE) to cluster strings by a pattern-aware similarity (hierarchical clustering… | ||
| Finding Code That Explodes Under Symbolic Evaluation | James Bornholt | 23m |
A profiler called SymPro constructs a symbolic evaluation graph and a symbolic heap to locate where symbolic evaluation explodes, implemented for Rosette and… | ||
| Concurrency-aware object-oriented programming with roles | Michael Faes | 25m |
A concurrency model makes every object carry a per-task role and enforces three concrete roles: readwrite role, readonly role, pure role. When sharing, objects… | ||
| Compositional Programming and Testing of Dynamic Distributed Systems | Ankush Desai | 22m |
Paper: https://dl.acm.org/citation.cfm?id=3276529
Real-world distributed systems are rarely built as a monolithic system. Instead, they are composed of… | ||
| Collapsible Contracts: Fixing a Pathology of Gradual Typing | Daniel Feltey | 22m |
Introduces collapsible contracts as a tree-structured replacement for opaque contract wrappers that merges new and existing contracts with a merge function… | ||
| BioScript: Programming Safe Chemistry on Laboratories-on-a-Chip | Mohsen Lesani | 24m |
A domain-specific language, BioScript targets digital microfluidic biochips and pairs a BioScript type system (models EPA’s 68 reactivity groups as union types… | ||
| Bidirectional Evaluation with Direct Manipulation | Mikaël Mayer | 25m |
Presents an algorithm that synthesizes program edits from direct output changes by retracing evaluation steps to rewrite a full ML-style functional program… | ||
| Beauty is the Promise of Happiness | Jenny Quillien | 01h 27m |
Argues that beauty is a creative force that resolves paradox at the edge and that designers must aim for human wellbeing, not just surface aesthetics. Uses… | ||
| Awards/SIGPLAN Town Hall Meeting | Jens Palsberg | 41m |
SIGPLAN reports spending $200,000 a year on travel grants for about 40 students per conference, offers gold open access paid for authors when needed, and asks… | ||
| Automatic Diagnosis and Correction of Logical Errors for Functional Programming Assignments | Junho Lee | 25m |
FixML is a tool that combines statistical error-localization with type-directed program synthesis plus component reduction and symbolic-execution pruning to… | ||
| AnyDSL: A Partial Evaluation Framework for Programming High-Performance Libraries | Roland Lei├Ła | 23m |
Claims an annotation-based, online partial evaluator over a CPS-style IR that drives code generation for vectorization/parallelization on CPUs and GPUs via… | ||
| A new modularity for software | Daniel Jackson | 01h 24m |
Proposes a practical modularity where user-facing "concepts" are the unit of design: each has a purpose, structure, actions and an operational principle… | ||
| An Empirical Study of the Effect of Source-level Loop Transformations on Compiler Stability | Zhangxiaowen Gong | 25m |
A systematic study extracts ~1,100 loop nests and generates 65,000 mutations via interchange, tiling, unrolling, rolling and distribution, then compiles with… | ||
| Cross-Component Garbage Collection | Michael Lippautz | 24m |
A generic algorithm called cross-component tracing extends V8’s tracer into Blink so the JavaScript heap can trace C++ DOM objects, requiring object and layout… | ||
| nothing matches | ||