OOPSLA 2023
2023-10-23..2023-10-27
Lisbon, Portugal
OOPSLA ·
[OOPSLA 2018, OOPSLA 2020, OOPSLA 2021, OOPSLA 2022, OOPSLA 2023, OOPSLA 2024, OOPSLA 2025]
| title | author | length |
|---|---|---|
| Opening and Welcome | Vash Vasalos | 19m |
Second-largest SPLASH in a dozen years with almost 40% students, eight colocated conferences and 10 workshops, about 30 organizers plus 50 student volunteers… | ||
| Scaling up machine learning without tears (and what do programming languages ha... | Dimitrios Vytiniotis | 01h 03m |
Concrete tooling that turns JAX-traced array programs into deployable sharding plans and fast estimates: a small DSL plus a simulator that reproduces published… | ||
| Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contrac... | Zhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, S. Hitarth | 18m |
Asparagus is a tool that takes Solidity/EVM bytecode, over-approximates it into polynomial transition systems, and synthesizes linear or polynomial parametric… | ||
| Equality Saturation Theory Exploration à la Carte | Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi | 15m |
Enumo is a domain-specific language for programmable theory exploration that gives users small, composable operators to guide automatic inference of rewrite… | ||
| Synthesizing Specifications | Kanghee Park, Loris D'Antoni, Thomas Reps | 19m |
Algorithm synthesizes all best L-properties that are sound, precise (no strictly more precise L-property exists), and complete (no further L-properties can… | ||
| Explainable Program Synthesis by Localizing Specifications | Amirmohammad Nazari, Yifei Huang, Roopsha Samanta, Arjun Radhakrishna, Mukund Raghothaman | 17m |
Introduces subspecifications that summarize what a subexpression must satisfy given a global spec, provides a two stage algorithm that constructs then… | ||
| Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction | Zhenyang Xu, Yongqiang Tian, Mengxiao Zhang, Gaosen Zhao, Yu Jiang, Chengnian Sun | 17m |
Vulcan is a language-agnostic postprocessor built on Perses that repeatedly applies three auxiliary reducers—identifier replacement, subtree replacement guided… | ||
| Grounded Copilot: How Programmers Interact with Code-Generating Models | Shraddha Barke, Michael B. James, Nadia Polikarpova | 18m |
Study watches 20 programmers across four tasks and languages and builds a grounded-theory claim that interactions with Copilot are bimodal: acceleration mode… | ||
| Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Progr... | Alex Renda, Yi Ding, Michael Carbin | 19m |
Method proposes Turaco, a tiny language plus analysis that computes per-path sample complexity from program source by forming a power series tilde… | ||
| Concrete Type Inference for Code Optimization using Machine Learning with SMT S... | Fangke Ye, Jisheng Zhao, Jun Shirako, Vivek Sarkar | 18m |
Introduces a hybrid pipeline that feeds GPT-4 style ML predictions into an SMT solver (CVC5) with a lexicographic scoring constraint to produce a bounded set… | ||
| An Explanation Method for Models of Code | Yu Wang, Ke Wang, Linzhang Wang | 17m |
An Explanation Method for Models of Code (Video, OOPSLA2 2023)
Yu Wang, Ke Wang, and Linzhang Wang
(Nanjing University, China; Visa Research, USA; Nanjing… | ||
| Optimization-Aware Compiler-Level Event Profiling | Matteo Basso, Aleksandar Prokopec, Andrea Rosà, Walter Binder | 19m |
Instrumentation lives inside Graal and delays insertion until after the last phase that can remove the event, using lightweight markers instead of… | ||
| Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates | Aalok Thakkar, Nathaniel Sands, George Petrou, Rajeev Alur, Mayur Naik, Mukund Raghothaman | 18m |
Mobius presents a concrete pipeline: seed a non‑recursive synthesizer, normalize the result, and perform iterative predicate unification guided by data… | ||
| Data Extraction via Semantic Regular Expression Synthesis | Qiaochu Chen, Arko Banerjee, Çağatay Demiralp, Greg Durrett, Işıl Dillig | 18m |
Smore implements semantic regexes that combine syntactic patterns with semantic predicates (dates, ranges, locations, person/org types) and synthesizes them by… | ||
| Synthesizing Efficient Memoization Algorithms | Yican Sun, Xuanyu Peng, Yingfei Xiong | 18m |
Automated synthesizer takes a MiniZinc-style declarative spec and produces a top-down memoization algorithm by extracting subproblems and synthesizing two… | ||
| Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Program... | Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, Harshit Jitendra Motwani | 17m |
Algorithm reduces template-based synthesis of polynomial imperative programs to Quadratic Programming by applying Farkas, Handelman, Putinar (SOS) and the Real… | ||
| Modular Component-Based Quantum Circuit Synthesis | Chan Gu Kang, Hakjoo Oh | 15m |
A synthesizer constructs quantum circuits from user-supplied component gates by performing enumerative search with pruning at the module-level search (modules… | ||
| Run-Time Prevention of Software Integration Failures of Machine Learning APIs | Chengcheng Wan, Yuhan Liu, Kuntai Du, Henry Hoffmann, Junchen Jiang, Michael Maire, Shan Lu | 18m |
SmartGear is a run-time adapter that sits between ML cloud APIs and application code, inserted via bytecode instrumentation, that detects… | ||
| Compiling Structured Tensor Algebra | Mahdi Ghorbani, Mathieu Huot, Shideh Hashemian, Amir Shaikhha | 20m |
Framework compiles tensor algebra while symbolically computing sparsity and redundancy at compile time, using an intermediate language STUR and a compiler… | ||
| Perception Contracts for Safety of ML-Enabled Systems | Angello Astorga, Chiao Hsieh, P. Madhusudan, Sayan Mitra | 20m |
Proposes Perception contracts — symbolic formulas that bound error between ground truth and perception estimates so a controller keeps a safety invariant — and… | ||
| Languages with Decidable Learning: A Meta-theorem | Paul Krogmeier, P. Madhusudan | 18m |
Proves a concrete meta-theorem: if a symbolic language admits a facet interpreter whose extra memory is bounded by the fixed structure (independent of… | ||
| Fluent APIs in Functional Languages | Ori Roth, Yossi Gil | 20m |
Claims a way to get fluent APIs in functional languages without name overloading by using parametric polymorphism and Hindley-Milner type inference and a… | ||
| A Pretty Expressive Printer | Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak | 17m |
Claims a new printer Πe that is strictly more expressive than prior pretty printers, provably minimizes a user-chosen optimality objective via a Cost Factory… | ||
| How Domain Experts Use an Embedded DSL | Lisa Rennels, Sarah E. Chasins | 19m |
An embedded DSL called Mimi targets climate-economics models and the paper reports a contextual inquiry with 9 participants; designers use Julia features like… | ||
| Saggitarius: A DSL for Specifying Grammatical Domains | Anders Miltner, Devon Loehr, Arnold Mong, Kathleen Fisher, David Walker | 17m |
Saggitarius defines metagrammars (DSLs whose denotation is a set of CFGs with existential parameters and constraints) and uses a generated giant grammar plus… | ||
| Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free P... | Huanqi Cao, Shizhi Tang, Qianchao Zhu, Bowen Yu, Wenguang Chen | 15m |
Mat2Stencil is a Python-embedded DSL that turns structured sparse matrices into matrix-free generalized stencils via type-based multi-stage compilation… | ||
| Translating canonical SQL to imperative code in Coq | Véronique Benzaken, Évelyne Contejean, Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jerome Simeon | 18m |
A mechanically verified compiler named DBCert translates a canonical SQL subset with correlated queries and NULL semantics into an imperative language using… | ||
| A Deductive Verification Infrastructure for Probabilistic Programs | Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja | 17m |
A deductive verification infrastructure implements an IVL (HAV/Halo) and a real-valued logic that encodes expectation-based specs, encodings for 12 loop proof… | ||
| A Gradual Probabilistic Lambda Calculus | Wenjia Ye, Matías Toro, Federico Olmedo | 19m |
Defines GPLC, a gradual probabilistic lambda calculus with probabilistic types and a binary choice operator, and elaborates programs to a target TPLC with… | ||
| Lower Bounds for Possibly Divergent Probabilistic Programs | Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan | 17m |
A proof rule called guard strengthening gives sound lower bounds for weakest preexpectations of possibly divergent probabilistic loops by replacing loop guards… | ||
| Exact Recursive Probabilistic Programming | David Chiang, Colin McDonald, Chung-chieh Shan | 16m |
A probabilistic programming compiler called Purple expresses unbounded recursion and then eliminates recursive data types using defunctionalization and… | ||
| Solving String Constraints with Lengths by Stabilization | Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Juraj Síč | 21m |
Combines a fast automata-based stabilization solver for equations+regular constraints with an align-and-split module to extract lengths, implements both in Z3… | ||
| Hydroflow: A Compiler Target for Fast, Correct Distributed Programs | Joseph M. Hellerstein | 01h 02m |
Hydroflow presents a Rust-based dataflow IR that compiles into networked transducer binaries, uses a semilattice formalism to make CRDT-style state composable… | ||
| The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilo... | Qinlin Chen, Nairen Zhang, Jinpeng Wang, Tian Tan, Chang Xu, Xiaoxing Ma, Yue Li | 18m |
Claim: a compact operational semantics captures Verilog’s tricky behaviors and serves as a reference. The work defines a λV core language that desugars real… | ||
| Regular Expression Matching using Bit Vector Automata | Alexis Le Glaunec, Lingkun Kong, Konstantinos Mamouras | 18m |
Presents a new automaton model called NBVA that simulates nondeterministic counter automata by manipulating per-state bit vectors, using rotations, single-bit… | ||
| Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Mani... | Xing Zhang, Guanchen Guo, Xiao He, Zhenjiang Hu | 18m |
Claims a first bidirectional object‑oriented language, BFJ, with a new backward semantics that handles ambiguous class‑hierarchy updates and mutable references… | ||
| Bring Your Own Data Structures to Datalog | Arash Sahebolamri, Langston Barrett, Scott Moore, Kristopher Micinski | 17m |
Claims a compiler and runtime that let analyses plug Bring Your Own Data Structures into a Datalog engine via a Rust embedded DSL and procedural macros, with a… | ||
| Reference Capabilities for Flexible Memory Management | Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad | 18m |
Verona organises all objects into tree-shaped regions with a window of mutability that only allows allocation and deallocation in the active region, making… | ||
| A Grounded Conceptual Model for Ownership Types in Rust | Will Crichton, Gavin Gray, Shriram Krishnamurthi | 19m |
Created an Ownership Inventory to measure Rust misconceptions and finds learners predict compiler errors 64% of the time but produce valid counterexamples only… | ||
| Inference of Resource Management Specifications | Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu K. Lahiri, Akash Lal, Manu Sridharan | 18m |
Automatic inference produces resource-management specs for Java and C# by applying optimistic inference rules framed in a Datalog-style fixpoint so the system… | ||
| Resource-Aware Soundness for Big-Step Semantics | Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca | 18m |
Extends a call-by-value language with grades that track resource use at evaluation time and a matching graded type system, proving that well-typed programs… | ||
| Verus: Verifying Rust Programs using Linear Ghost Types | Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel | 18m |
Verus is an SMT-based verifier that embeds proofs in Rust and uses linear ghost permissions to represent ownership-aligned memory permissions; the tool demands… | ||
| The Bounded Pathwidth of Control-Flow Graphs | Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Chun Kit Lam | 17m |
Proves control-flow graphs of structured, goto-free programs have pathwidth at most 2·nesting depth, and gives a linear-time path decomposition construction… | ||
| How Profilers Can Help Navigate Type Migration | Ben Greenman, Matthias Felleisen, Christos Dimoulas | 18m |
Uses a 16‑benchmark corpus with ~100,000 gradually typed configurations and 1.2M runtime/profile measurements to evaluate 17 migration strategies driven by a… | ||
| Synthesizing Precise Static Analyzers for Automatic Differentiation | Jacob Laurel, Siyuan Brant Qian, Gagandeep Singh, Sasa Misailovic | 17m |
Pasado synthesizes precise static analyzers that directly abstract the Chain Rule, Product Rule and Quotient Rule in automatic differentiation, producing a… | ||
| A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitiv... | Dongjie He, Yujiang Gui, Wei Li, Yonggang Tao, Changwei Zou, Yulei Sui, Jingling Xue | 18m |
A new preanalysis called DebloaterX uses three container-usage patterns and a limited field sensitive DFA to mark container objects as context dependent or… | ||
| Static Analysis of Memory Models for SMT Encodings | Thomas Haas, René Maseli, Roland Meyer, Hernán Ponce de León | 18m |
A static analysis computes per-execution upper and relativized lower bounds on memory-model relations (program order, coherence, read-from) and propagates them… | ||
| Greedy Implicit Bounded Quantification | Chen Cui, Shengyi Jiang | 18m |
Presents F≤b, a variant of kernel F≤ with greedy implicit instantiation that handles bounded quantification, interdependent bounds, higher-rank polymorphism… | ||
| Structural Subtyping as Parametric Polymorphism | Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley | 17m |
Compares structural subtyping for records and variants with row and presence polymorphism and gives compositional translations that preserve types and… | ||
| Mutually Iso-Recursive Subtyping | Andreas Rossberg | 19m |
Shows the classic Amber rule forces an exponential encoding for mutually recursive iso-recursive types and instead defines a core calculus with declared upper… | ||
| Getting into the Flow: Towards Better Type Error Messages for Constraint-Based ... | Ishan Bhanuka, Lionel Parreaux, David Binder, Jonathan Immanuel Brachthäuser | 20m |
Proposes turning constraint-generation into explicit data flows by attaching provenances (sequences of source locations) to algebraic subtyping constraints… | ||
| Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af... | Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, Tiark Rompf | 18m |
A typed graph IR combines reachability types with an effect system to compute precise, flow-sensitive effect dependencies without CFA by doing type-based… | ||
| AST vs. Bytecode: Interpreters in the Age of Meta-Compilation | Octave Larose, Sophie Kaleba, Humphrey Burchell, Stefan Marr | 17m |
Four interpreters (AST and bytecode implemented atop RPython and GraalVM/Truffle, running the SOM micro-language) compare interpreter performance, JIT peak… | ||
| Reusing Just-in-Time Compiled Code | Meetesh Kalpesh Mehta, Sebastián Krynski, Hugo Musso Gualandi, Manas Thakur, Jan Vitek | 19m |
An experimental JIT called Ř is extended to record compiled functions into a persistent curated code repository and later replay matching versions to skip… | ||
| TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism | Matt D'Souza, James You, Ondřej Lhoták, Aleksandar Prokopec | 17m |
TASTyTruffle interprets Scala TASTy (not JVM bytecode), reifies generic types as runtime shapes and implements heterogeneous box-free representations so… | ||
| Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic ... | Girish Mururu, Sharjeel Khan, Bodhisatwa Chatterjee, Chao Chen, Chris Porter, Ada Gavrilovska, Santosh Pande | 22m |
Compiler and runtime build a pipeline that instruments loops with “beacons” carrying predicted loop trip count, timing, memory footprint and reuse-distance… | ||
| Historia: Refuting Callback Reachability with Message-History Logics | Shawn Meier, Sergio Mover, Gowtham Kaki, Bor-Yuh Evan Chang | 18m |
Defines message histories (sequences of boundary call-ins/callbacks) and a temporal message-history logic, implements a prototype verifier called Historia that… | ||
| Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-... | Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Kerim Kochekov, Yun Chen Tsai, Ahmed Khaled Zaher | 17m |
Claims an on-demand APA pipeline that, after n·log n·k preprocessing, answers any pairwise path-summary query in O(k) per query by precomputing only O(n log n)… | ||
| A Cocktail Approach to Practical Call Graph Construction | Yuandao Cai, Charles Zhang | 18m |
Build named Coral prototype combines a cheap pre-analysis, a two-stage flow-insensitive pipeline and selective expensive refinement to resolve function-pointer… | ||
| 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, Jiaguang Sun | 19m |
Builds a runtime system-call sandbox called DBox that instruments program binaries to gradually disable system calls at identified reduction points using… | ||
| Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection | Ruyi Ji, Chaozhe Kong, Yingfei Xiong, Zhenjiang Hu | 16m |
Proposes LearnSy, a question selector that models complex operator behavior as simple random events and computes the expected number of program pairs that… | ||
| Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect... | Magnus Madsen, Jaco van de Pol, Troels Henriksen | 18m |
Presents a hybrid solver that combines Boole’s SVE elimination with binary decision diagrams plus precomputed tabling and caching; implemented in the Flix… | ||
| From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect ... | Marius Müller, Philipp Schuster, Jonathan Lindegaard Starup, Klaus Ostermann, Jonathan Immanuel Brachthäuser | 19m |
A typed, semantics- and typability-preserving lift-inference translation converts a source language with second-class capabilities into a region calculus that… | ||
| Gradual Typing for Effect Handlers | Max S. New, Eric Giovannini, Daniel R. Licata | 18m |
GrEff is a gradually typed language for effect handlers that supports incremental migration from unchecked to checked effect typing; it elaborates to a cast… | ||
| When Concurrency Matters: Behaviour-Oriented Concurrency | Luke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias, Sophia Drossopoulou, David Chisnall, Tobias Wrigstad, Paul Liétar | 16m |
Behaviour-Oriented Concurrency (BoC) introduces cones as exclusive shared-data owners, behaviors as spawned units that declare required cones, and a single… | ||
| Continuing WebAssembly with Effect Handlers | Luna Phipps-Costin, Andreas Rossberg, Arjun Guha, Daan Leijen, Daniel Hillerström, KC Sivaramakrishnan, Matija Pretnar, Sam Lindley | 18m |
WasmFX extends WebAssembly with WasmFX adds three instructions to create, suspend and resume continuations and with typed one-shot continuations that fit… | ||
| All the Languages Together | Amal Ahmed | 01h 05m |
Proposes a proof technique that builds a semantic intermediate representation (logical relations of source types as sets of target terms) to verify FFI glue… | ||
| Towards Better Semantics Exploration for Browser Fuzzing | Chijin Zhou, Quan Zhang, Lihua Guo, Mingzhe Wang, Yu Jiang, Qing Liao, Zhiyong Wu, Shanshan Li, Bin Gu | 17m |
SaGe automatically extracts a CFG from W3C specs, refines it with browser-execution feedback into a production-context sensitive grammar so the fuzzer avoids… | ||
| Live Pattern Matching with Typed Holes | Yongwei Yuan, Scott Guest, Eric Griffis, Hannah Potter, David Moon, Cyrus Omar | 19m |
Supports exhaustiveness and redundancy checking for patterns that contain holes, maps those checks to first-order constraint entailments, and proves decidable… | ||
| Interactive Debugging of Datalog Programs | André Pacak, Sebastian Erdweg | 17m |
Claims the first small-step operational semantics for top-down (query/subquery) Datalog, formalizing where a debugger can stop; implements a debugger for core… | ||
| Accelerating Fuzzing through Prefix-Guided Execution | Shaohua Li, Zhendong Su | 18m |
Introduces prefix-guided execution that monitors a test's partial run (a sequence of basic block IDs) and applies early termination when the prefix is already… | ||
| MemPerf: Profiling Allocator-Induced Performance Slowdowns | Jin Zhou, Sam Silvestro, Steven (Jiaxun) Tang, Hanmei Yang, Hongyu Liu, Guangming Zeng, Bo Wu, Cong Liu, Tongping Liu | 19m |
MemPerf is a profiler that pinpoints allocator-induced slowdowns by modeling heap-object life cycles and distinguishing slow management operations from slow… | ||
| Initializing Global Objects: Time and Order | Fengyun Liu, Ondřej Lhoták, David Hua, Enze Xing | 18m |
Claims a static, flow-sensitive interprocedural analysis that enforces initialization-time irrelevance plus partial ordering to eliminate Scala global-object… | ||
| Type-Safe Dynamic Placement with First-Class Placed Values | George Zakhour, Pascal Weisenburger, Guido Salvaneschi | 16m |
A new DSL called Dyno implements placement types with union placement and first-class remote refs, letting the compiler statically track values that may live… | ||
| Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data | Thierry Renaux, Sam Van den Vonder, Wolfgang De Meuter | 18m |
A system called Secure RDTs enforces role‑based read/write rules on offline JSON by projecting a server‑specified policy and per‑role data excerpts to clients… | ||
| AtomiS: Data-Centric Synchronization Made Practical | Hervé Paulino, Ana Almeida Matos, Jan Cederquist, Marco Giunti, João Matos, António Ravara | 20m |
AtomiS implements a Java data-centric synchronization model that requires only qualified types on interfaces and fields, then runs a static analysis to infer… | ||
| Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based S... | Christopher Wagner, Nouraldin Jaber, Roopsha Samanta | 21m |
Presents Venus, an implementation that extends Quicksilver to verify systems that are unbounded in both process count and data by reducing variable domains via… | ||
| Solving Conditional Linear Recurrences for Program Verification: The Periodic C... | Chenglin Wang, Fangzhen Lin | 15m |
Shows that a conditional linear recurrence has a computable closed form whenever its ultimately periodic index sequence holds, proves checking that property is… | ||
| Melocoton: A Program Logic for Verified Interoperability Between OCaml and C | Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer | 18m |
Melocoton claims the first formal semantics of the OCaml FFI and the first multi‑language program logic that reasons about OCaml and C interactions… | ||
| Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasonin... | Noam Zilberstein, Derek Dreyer, Alexandra Silva | 15m |
Outcome Logic (OL) replaces a single postcondition with outcome-indexed assertions over sets of states, adds an outcome conjunction that composes reachable… | ||
| Formal Abstractions for Packet Scheduling | Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, Dexter Kozen | 17m |
Formal operational semantics for PIFO trees and a new notion called homomorphic embedding show when one tree can reproduce another’s packet permutations… | ||
| P4R-Type: A Verified API for P4 Control Plane Programs | Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller, Alceste Scalas | 19m |
Library implements a verified Scala API that encodes P4Info as Scala types and statically rejects mismatches between P4 tables, allowed actions, and action… | ||
| Compositional Security Definitions for Higher-Order Where Declassification | Jan Menz, Andrew K. Hirsch, Peixuan Li, Deepak Garg | 19m |
Defines a compositional security notion for where declassification in higher-order languages by building an indistinguishability logical relation that stops… | ||
| Fat Pointers for Temporal Memory Safety of C | Jie Zhou, John Criswell, Michael Hicks | 17m |
Extends Checked C with four new fat pointers that store a key and an offset and enforces temporal safety via dynamic key-lock checks; implements… | ||
| Quantifying and Mitigating Cache Side Channel Leakage with Differential Set | Cong Ma, Dinghao Wu, Gang Tan, Mahmut Taylan Kandemir, Danfeng Zhang | 17m |
Introduces a new abstraction differential set and a tool DSA that both measures and removes cache side‑channel leakage by aligning sibling memory accesses… | ||
| A Verification Methodology for the Arm® Confidential Computing Architecture: Fr... | Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, Nathan Chong | 19m |
The project verifies Arm CCA’s Realm Management Monitor by combining CBMC model checking, interactive theorem proving, and concurrency-aware testing against a… | ||
| Verifying Indistinguishability of Privacy-Preserving Protocols | Kirby Linvill, Gowtham Kaki, Eric Wustrow | 18m |
Library Waldo implements a middle ground between symbolic and computational models in F by modeling messages as bitstrings, using a tape to factor out… | ||
| Formally Verifying Optimizations with Block Simulations | Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard | 19m |
Framework implements block-level forward simulations inside CompCert and proves validators in the Coq proof assistant that check concrete morphisms between… | ||
| Back to Direct Style: Typed and Tight | Marius Müller, Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann | 15m |
Two typed languages are presented: a direct-style language and a CPS language, each with an abstract-machine semantics, plus translations both ways that are… | ||
| Hardware-Aware Static Optimization of Hyperdimensional Computations | Pu (Luke) Yi, Sara Achour | 18m |
Heim is a hardware-aware static optimizer for BSC hyperdimensional computing that analytically derives the minimum hypervector size and distance thresholds and… | ||
| Rapid: Region-Based Pointer Disambiguation | Khushboo Chitre, Piyus Kedia, Rahul Purandare | 18m |
A tool called Rapid uses a profiler + region-based allocator to place hot allocation sites into disjoint regions of 4GB-aligned segments so dynamic checks test… | ||
| Automated Ambiguity Detection in Layout-Sensitive Grammars | Jiangyi Liu, Fengmin Zhu, Fei He | 17m |
Extends bounded-ambiguity SAT methods to layout-sensitive grammars by replacing SAT with SMT+Z3 and adding a reachability condition to fix a discovered… | ||
| Stuttering for Free | Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, Derek Dreyer | 17m |
Presents FreeSim, a new stuttering-simulation technique mechanized in Coq that replaces the usual “synchronous progress” requirement with asynchronous… | ||
| Complete First-Order Reasoning for Properties of Functional Programs | Adithya Murali, Lucas Peña, Ranjit Jhala, P. Madhusudan | 19m |
The paper proves that the unfolding-then-SMT procedure (USMT heuristic) used by Liquid Haskell, Leon and Stainless is sound and complete for the combined… | ||
| Counterexample Driven Quantifier Instantiations with Applications to Distribute... | Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv | 16m |
Replaces problematic function symbols with a one-to-one relational abstraction inside Ivy and drives refinements by solver counterexamples; SMT solvers that… | ||
| A conceptual framework for safe object initialization: a principled and mechani... | Clément Blaudeau, Fengyun Liu | 20m |
Defines four enforceable principles—monotonicity, authority, stackability, scopability—and builds a small Celsius calculus that encodes temperature-annotated… | ||
| Verification-Preserving Inlining in Automatic Separation Logic Verifiers | Thibault Dardinier, Gaurav Parthasarathy, Peter Müller | 20m |
Presents a provable criterion that makes bounded inlining safe for automatic separation-logic verifiers: a semantic condition (formalized in Isabelle/HOL) that… | ||
| Leaf: Modularity for Temporary Sharing in Separation Logic | Travis Hance, Jon Howell, Oded Padon, Bryan Parno | 19m |
Claims a single abstraction that encodes temporary read sharing across different permission systems and shows it works concretely: a guarding operator that… | ||
| Proof Automation for Linearizability in Separation Logic | Ike Mulder, Robbert Krebbers | 19m |
Implements proof automation for contextual refinement and logical atomicity inside Diaframe 2.0, encoded in Iris and Coq, and uses both program shape and… | ||
| Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic | Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon Kang | 17m |
Proposes modular, machine-checked specs for hazard pointers and RCU and proves realistic reclamation implementations in Coq, mechanized in Iris. Claims… | ||
| Functional collection programming with semi-ring dictionaries | Amir Shaikhha, Mathieu Huot, Jaclyn Smith, Dan Olteanu | 20m |
A new intermediate language implements semi-ring dictionaries and a statically typed DSL SDQL that represents sets, multisets, vectors, matrices and sparse… | ||
| Aliasing Limits on Translating C to Safe Rust | Mehmet Emre, Peter Boyland, Aesha Parekh, Ryan Schroeder, Kyle Dewey, Ben Hardekopf | 18m |
Study measures how many C raw pointers can become Rust safe references after ownership/lifetime inference, using a modified C→unsafe-Rust transpile pipeline… | ||
| Adventure of a Lifetime: Extract Method Refactoring for Rust | Sewen Thy, Andreea Costea, Kiran Gopinathan, Ilya Sergey | 17m |
An automated pipeline hoists a candidate function then applies staged repairs to satisfy Rust ownership and lifetimes, implemented as an IntelliJ Rust plugin… | ||
| Inductive Program Synthesis Guided by Observational Program Similarity | Jack Feser, Işıl Dillig, Armando Solar-Lezama | 18m |
Introduces SyMetric, a tool that replaces observational equivalence with a domain-specific observational similarity metric to cluster programs into… | ||
| Automated Translation of Functional Big Data Queries to SQL | Guoqiang Zhang, Benjamin Mariano, Xipeng Shen, Işıl Dillig | 14m |
Translates Spark RDD-style functional queries to SQL using counterexample-guided inductive synthesis plus a novel column-wise decomposition that extracts… | ||
| User-Customizable Transpilation of Scripting Languages | Bo Wang, Aashish Kolluri, Ivica Nikolić, Teodora Baluta, Prateek Saxena | 22m |
A prototype called DuoGlot translates Python to JavaScript by synthesizing syntactic translation rules from user-provided code snippets and composing them… | ||
| Hybrid Multiparty Session Types: Compositionality for Protocol Specification th... | Lorenzo Gheri, Nobuko Yoshida | 18m |
Claims a semantics-preserving method to compose separately-designed subprotocols into a single well-formed global MPST, introduces hybrid types that mix global… | ||
| Mechanizing Session-Types using a Structural View: Enforcing Linearity without ... | Chuta Sano, Ryan Kavanagh, Brigitte Pientka | 19m |
Claims a method that removes linear contexts by embedding linearity as local predicates, mechanizes a session-typed CP variant called structural classical… | ||
| Message Chains for Distributed System Verification | Federico Mora, Ankush Desai, Elizabeth Polgreen, Sanjit A. Seshia | 17m |
Defines message chains as a listlike datatype that records send history so proofs avoid reasoning about individual messages or buffers, and implements an… | ||
| Randomized Testing of Byzantine Fault Tolerant Algorithms | Levin N. Winter, Florena Buse, Daan de Graaf, Klaus von Gleissenthall, Burcu Kulahcioglu Ozkan | 18m |
ByzzFuzz is a randomized tester that injects bounded faults (F faulty processes, D network perturbation rounds, C mutation rounds) and applies small-scope… | ||
| Validating IoT Devices with Rate-Based Session Types | Grant Iraci, Cheng-En Chuang, Raymond Hu, Lukasz Ziarek | 18m |
Framework formalizes rate-based session types by adding a periodic recursion Omega that records per-channel periods, proves preservation and rate error… | ||
| Awards and SPLASH 2024 | Tony Hosking | 20m |
OOPSLA recognizes the 2013 most influential paper, "Empirical Analysis of Programming Language Adoption," and announces award winners plus conference plans… | ||
| Deep Learning Robustness Verification for Few-Pixel Attacks | Yuval Shapira, Eran Avneri, Dana Drachsler Cohen | 18m |
Introduces Calzone, an L0 robustness verifier that gives sound and complete proofs by converting t-pixel neighborhoods into box (L-inf) queries and using… | ||
| 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, Sam Tobin-Hochstadt | 19m |
Rhombus is a new language implemented on Racket that replaces prefix s-exprs with an infix-friendly Shrubbery token-tree, interleaves macro expansion with an… | ||
| Simple Reference Immutability for System F-sub | Edward Lee, Ondřej Lhoták | 15m |
Presents a formal calculus extending System F_sub with a runtime seal operator that enforces transitive reference immutability, models records as mutable… | ||
| nothing matches | ||