OOPSLA 2024
2024-10-20..2024-10-25
Pasadena, United States
OOPSLA ·
[OOPSLA 2018, OOPSLA 2020, OOPSLA 2021, OOPSLA 2022, OOPSLA 2023, OOPSLA 2024, OOPSLA 2025]
who it's for
programming language researchers, compiler engineers, static analysis engineers, program verification engineers, language tool developers, programming language educators, software security researchers
topics
type inference logics; alias-aware IFDS analysis; effect handlers via coroutines; python to statically typed IR; sparse tensor auto-scheduling; llm-assisted compiler fuzzing; bounded SQL equivalence verification; memory-safe WebAssembly verification; probabilistic and Bayesian program analysis; multithreaded replay and record-replay
| title | author | length |
|---|---|---|
| Profiling Programming Language Learning | Will Crichton, Shriram Krishnamurthi | 24m |
Year‑long experiment embeds 221 quizzes in The Rust Programming Language and collects 62,526 readers answering 1,140,202 questions to locate learning hotspots… | ||
| PyDex: Repairing Bugs in Introductory Python Assignments using LLMs | Jialu Zhang, José Pablo Cambronero, Sumit Gulwani, Vu Le, Ruzica Piskac, Gustavo Soares, Gust Verbruggen | 19m |
PyDex is an APR pipeline that uses Codex with iterative prompts, parser diagnostics, test-case filtering, and peer-program few-shots to repair student Python… | ||
| Identifying and Correcting Programming Language Behavior Misconceptions | Kuang-Chen Lu, Shriram Krishnamurthi | 19m |
A curated list of dozen-plus concrete misconceptions about mutable variables, scope, aliasing and closures is paired with an instrument that detects them by… | ||
| HiPy: Extracting High-Level Semantics From Python Code For Data Processing | Michael Jungmair, Alexis Engelke, Jana Giceva | 21m |
HiPy converts annotated Python functions into program generators that, when executed, produce a statically-typed IR (SSA-like, n‑dimensional arrays and table… | ||
| Forge: A Tool and Language for Teaching Formal Methods | Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen, Charlie Cutting, Thomas Del Vecchio, Sidney LeVine, Julianne Rudner, Benjamin Ryjikov, Alexander Varga, Andrew Wagner, Luke West, Shriram Krishnamurthi | 20m |
Forge is a reworked Alloy designed to teach formal methods incrementally: it implements language levels (froglet → relational → LTL) that restrict expressive… | ||
| Unifying Static and Dynamic Intermediate Languages for Accelerator Generators | Caleb Kim, Pai Li, Anshuman Mohan, Andrew Butt, Adrian Sampson, Rachit Nigam | 20m |
Piezo is an IL that embeds static timing inside a dynamic Calyx-style language by treating static control as a refinement of dynamic behavior so the compiler… | ||
| The Ultimate Conditional Syntax | Luyu Cheng, Lionel Parreaux | 18m |
Proposes a new pattern syntax that combines conditional splits, pattern flowing, and interleaved let bindings; implements it in MLscript with an online… | ||
| Multiverse Notebook: Shifting Data Scientists to Time Travelers | Shigeyuki Sato, Tomoki Nakamaru | 19m |
Multiverse Notebook implements fork per cell kernel checkpoints so each cell runs in a child process and time-traveling is just forking a new child, avoiding… | ||
| Deriving Dependently-Typed OOP from First Principles | David Binder, Ingo Skupin, Tim Süberkrüb, Klaus Ostermann | 19m |
Derives a dependently typed object-oriented fragment by duality and gives a concrete calculus with two symmetric language fragments plus type- and… | ||
| A Case for First-Class Environments | Jinhao Tan | 18m |
Argues that a small-step environment-based semantics replaces substitution and yields λE, a call-by-value, statically typed calculus using de Bruijn indices… | ||
| UniSparse: An Intermediate Language for General Sparse Format Customization | Jie Liu, Zhongyuan Zhao, Zijian Ding, Benjamin Brock, Hongbo Rong, Zhiru Zhang | 19m |
UniSparse is an MLIR-based intermediate language and compiler that encodes sparse formats as a metadata tree plus a separate memory layout, implements… | ||
| The ART of Sharing Points-to Analysis: Reusing Points-to Analysis Results Safely and(…) | Shashin Halalingaiah, Vijay Sundaresan, Daryl Maier, V Krishna Nandivada | 19m |
A scheme called ART encodes flow-sensitive, context-insensitive points-to results so a consumer can regenerate them without recomputing fixed points and verify… | ||
| Boosting the Performance of Alias-Aware IFDS Analysis with CFL-based Environment(…) | Haofeng Li, Chenghang Shi, Jie Lu, Lian Li, Jingling Xue | 18m |
Reinterprets access-path generation as a Context-Free Language and casts field sensitivity as an IDE problem, implements the idea in IDEDroid and compares it… | ||
| A Learning-Based Approach to Static Program Slicing | Aashish Yadavally, Yi Li, Shaohua Wang, Tien N. Nguyen | 19m |
NS-Slicer uses a pre-trained language model to produce statement embeddings and two small classifiers that predict per-statement inclusion in backward or… | ||
| Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…) | Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, Tiark Rompf | 19m |
Presents a type system that adds a freshness qualifier to reachability types so newly allocated values remain distinct until substituted, enabling precise… | ||
| Type Inference Logics | Denis Carnier, François Pottier, Steven Keuchel | 19m |
Shows how to verify practical, imperative-style, constraint-based type inference that emits elaborated terms by separating constraint generation (implemented… | ||
| Refinement Type Refutations | Robin Webbers, Klaus von Gleissenthall, Ranjit Jhala | 21m |
Systematically turns bidirectional refinement type rules into refutations and defines must-instantiation as the concrete set of term inhabitants that prove a… | ||
| Qualifying System F-sub | Edward Lee, Yaoyu Zhao, Ondřej Lhoták, James You, Kavin Satheeskumar, Jonathan Immanuel Brachthäuser | 18m |
Paper claims a practical calculus System F<:Q that combines higher‑rank bounded polymorphism with a free lattice encoding of qualifier expressions, giving… | ||
| Intensional Functions | Zachary Palmer, Nathaniel Wesley Filardo, Ke Wu | 19m |
Adds a language feature that makes runtime closures visible: functions carry a definition-site ID and an environment and offer three destructors — application… | ||
| Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials | Nikhil Pimpalkhare, Zachary Kincaid | 21m |
Computes the best VASR reflection that linearly simulates the program, then exactly solves context-free-language reachability over that VASR to get procedure… | ||
| Model Checking Distributed Protocols in Must | Constantin Enea, Dimitra Giannakopoulou, Michalis Kokologiannakis, Rupak Majumdar | 20m |
Must is a bounded model checker that verifies real distributed implementations by instrumenting a mainstream language (example: Rust) with a tiny concurrency… | ||
| Mechanizing the CMP Abstraction for Parameterized Verification | Yongjian Li, Bohua Zhan, Jun Pang | 21m |
Provides a machine-checked formalization of the CMP abstraction with syntax-directed abstraction and strengthening rules proven sound in Isabelle/HOL… | ||
| Scaling Abstraction Refinement for Program Analyses in Datalog Using Graph Neural(…) | Zhenyu Yan, Xin Zhang, Peng Di | 21m |
Applies graph neural networks to Datalog-derived graphs to prune abstraction parameters, then solves the reduced max‑sat refinement problem with a solver… | ||
| Making Formulog Fast: An Argument for Unconventional Datalog Evaluation | Aaron Bembenek, Michael Greenberg, Stephen Chong | 19m |
Compiles Formulog to Soufflé and replaces semi-naive batching with eager evaluation, a concurrent work stealing DFS that specializes rules on novel facts and… | ||
| Finding Cross-rule Optimization Bugs in Datalog Engines | Chi Zhang, Linzhang Wang, Manuel Rigger | 17m |
Automated blackbox testing uses Incremental Rule Evaluation (IRE) to build Datalog programs rule by rule, evaluate each new rule in isolation as a reference… | ||
| A Typed Multi-Level Datalog IR and its Compiler Framework | David Klopp, Sebastian Erdweg, André Pacak | 21m |
A compiler framework implements a typed multi-level Datalog IR in Scala, formalizing a bipolar, flow-sensitive type system with three-valued contexts that both… | ||
| Verification of Neural Networks' Global Robustness | Anan Kabaha, Dana Drachsler Cohen | 16m |
Introduces Delta Global robustness as the minimal confidence margin guaranteeing any input stays correctly classified under a given perturbation, and builds an… | ||
| TorchQL: A Programming Framework for Integrity Constraints in Machine Learning | Aaditya Naik, Adam Stein, Yinjun Wu, Mayur Naik, Eric Wong | 19m |
TorchQL is a PyTorch-integrated query framework that expresses model errors as integrity-constraint violations and ships eight core operators to write those… | ||
| Extending the C/C++ Memory Model with Inline Assembly | Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad | 20m |
A formal memory model is built that extends RC11 to handle inline x86 assembly, specifically first C++ model with inline assembly for x86 covering non-temporal… | ||
| libLISA: Instruction Discovery and Analysis on x86-64 | Jos Craaijo, Freek Verbeek, Binoy Ravindran | 16m |
libLISA automatically discovers and synthesizes x86-64 instruction semantics by observing execution and inferring operand encodings, producing a CPU-specific… | ||
| Jmvx: Fast Multi-threaded Multi-Version eXecution and Record-Replay for Managed Languages | David Schwartz, Ankith Kowshik, Luís Pina | 18m |
Jmvx instruments Java bytecode to intercept native and nondeterministic library calls (found via strace signals), implements a lock‑free shared mmap ring… | ||
| HybridSA: GPU Acceleration of Multi-Pattern Regex Matching using Bit Parallelism | Alexis Le Glaunec, Lingkun Kong, Konstantinos Mamouras | 19m |
HybridSA is a heterogeneous CPU–GPU engine that compiles regexes (Glushkov NFAs) into bit masks and runs bit-parallel shift-and extensions as many small CUDA… | ||
| Fast and Optimal Extraction for Sparse Equality Graphs | Amir Kafshdar Goharshady, Chun Kit Lam, Lionel Parreaux | 20m |
The paper proves e-graph extraction is NP-hard and hard to approximate by reduction from set cover, then gives a fixed-parameter tractable dynamic program over… | ||
| Practical Verification Of Smart Contracts Using Memory Splitting | Shelly Grossman, Alexander Bakst, Sameer Arora, John Toman, Chandrakana Nandi, Mooly Sagiv | 21m |
The paper implements a conservative memory analysis and a memory-splitting transformation for EVM bytecode, integrated into CertoraProver, that recovers… | ||
| Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations | Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, John Wickerson | 18m |
Tooling and results: a new testing technique compiles individual C/C++ atomic operations with multiple mappings, links the permutations, and checks whether… | ||
| Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning | Gabriel Ryan, Burcu Cetin, Christian Yongwhan Lim, Suman Jana | 18m |
A system called HBFourier uses sparse Fourier learning to predict feasibility of ordered memory-access pairs from a coverage-guided trace corpus, estimating… | ||
| Automatically Reducing Privilege for Access Control Policies | Loris D'Antoni, Shuo Ding, Amit Goel, Mathangi Ramesh, Neha Rungta, Chungha Sung | 19m |
Tool named IAM-PolicyRefiner synthesizes tighter AWS IAM policies from three months of real access logs, removing on average 77% of allowed actions and 88% of… | ||
| Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types | Aleksander Boruch-Gruszecki, Adrien Ghosn, Mathias Payer, Clément Pit-Claudel | 19m |
Proposal implements a Scala extension called Gradient that lets legacy code be migrated incrementally to an object-capability model by combining runtime… | ||
| Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation | Qianchuan Ye, Benjamin Delaware | 19m |
A new MPC language called Taypsi compiles ordinary functional programs with recursive ADTs into policy-respecting oblivious implementations using a lifting… | ||
| Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification | Taro Sekiyama, Hiroshi Unno | 22m |
Claims decidability for higher-order model checking of programs with algebraic effect handlers by statically bounding the number of simultaneously active… | ||
| Lexical Effect Handlers, Directly | Cong Ma, Zhaoyi Ge, Edward Lee, Yizhou Zhang | 18m |
Compiles lexically scoped algebraic effect handlers down to low-level stack switching and header frames, identifying handlers by memory address so handler… | ||
| Effects and Coeffects in Call-By-Push-Value | Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, Stephanie Weirich | 19m |
Presents a type system for call-by-push-value that statically bounds both observable effects and environmental demands and proves effect-and-coeffect soundness… | ||
| Effect handlers for C via coroutines | Mario Alvarez-Picallo, Teodoro Freund, Dan Ghica, Sam Lindley | 20m |
libseff implements effect handlers for C by representing pending computations as mutable coroutines and dispatching on reified operations (no closures)… | ||
| Persimmon: Nested Family Polymorphism with Extensible Variant Types | Anastasiya Kravchuk-Kirilyuk, Gary Feng, Jonas Iskander, Yizhou Zhang, Nada Amin | 20m |
Persimmon implements nested family polymorphism with extensible variant types, using a linkage concatenation representation to combine inherited and new… | ||
| Merging Gradual Typing | Wenjia Ye, Matías Toro | 20m |
A new λM⋆ calculus combines gradual typing with an intersection-based merge operator, gives a typed-driven runtime (no separate cast calculus), and formalizes… | ||
| Gradually Typed Languages Should Be Vigilant! | Olek Gierczak, Lucy Menon, Christos Dimoulas, Amal Ahmed | 19m |
Defines vigilance as a semantic criterion that checks whether runtime enforcement preserves the full run-time typing history; implements it by instrumenting… | ||
| Full Iso-recursive Types | Litao Zhou, Qianyong Wan | 16m |
Presents a new formulation called λFiµ that replaces iso-recursive fold/unfold with general erasable casts so equi-recursive programs encode without runtime… | ||
| Degrees of Separation: A Flexible Type System for Safe Concurrency | Yichen Xu, Aleksander Boruch-Gruszecki, Martin Odersky | 20m |
A new calculus, Capture Separation Calculus (System CSC), tracks aliases via capturing types and lets code run unmodified by default but enforces separation… | ||
| Tachis: Higher-Order Separation Logic with Credits for Expected Costs | Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal | 17m |
Tachis introduces probabilistic cost credits, a separation logic resource that preserves expectation across random branches and lets proofs allocate credits… | ||
| Sensitivity by Parametricity | Elisabet Lobo-Vesga, Carlos Tomé Cortiñas, Alejandro Russo, Marco Gaboardi | 16m |
A method reduces proving a function’s sensitivity to ordinary type-checking by encoding metric relations at the type level and exploiting parametric… | ||
| Quantitative Bounds on Resource Usage of Probabilistic Programs | Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Đorđe Žikelić | 18m |
Extends cost supermartingales to yield sound expectation bounds for programs with positive and negative costs and unbounded updates provided a lower bounded… | ||
| Programmable MCMC with Soundly Composed Guide Programs | Long Pham, Di Wang, Feras A. Saad, Jan Hoffmann | 19m |
Implements a coroutine-based framework and a type system that encodes the message protocol between a model program and a sequence of block-wise guide programs… | ||
| Statistical Testing of Quantum Programs via Fixed-Point Amplitude Amplification | Chan Gu Kang, Joonghoon Lee, Hakjoo Oh | 18m |
Proposes using fixed-point amplitude amplification to reduce the number of runs needed to statistically detect wrong output states, claiming reductions like… | ||
| Rustlantis: Randomized Differential Testing of the Rust Compiler | Qian (Andy) Wang, Ralf Jung | 19m |
Rustlantis is a randomized differential fuzzer that generates MIR directly and targets rustc backends (LLVM and Cranelift) plus Miri to detect UB. It… | ||
| Reward Augmentation in Reinforcement Learning for Testing Distributed Systems | Andrea Borgarelli, Constantin Enea, Rupak Majumdar, Srinidhi Nagendra | 18m |
Paper proposes using reinforcement learning to bias randomized testing of real consensus implementations, implemented in Go, by adding a decaying exploration… | ||
| Drowzee: Metamorphic Testing for Fact-conflicting Hallucination Detection in Large(…) | Ningke Li, Yuekang Li, Yi Liu, Ling Shi, Kailong Wang, Haoyu Wang | 19m |
Drowzee is a logic-programming–driven metamorphic tester that crawls Wikipedia to build a KB, applies Prolog rules (negation, symmetric, inverse, transitive… | ||
| Crabtree: Rust API Test Synthesis Guided by Coverage and Type | Yoshiki Takashima, Chanhee Cho, Ruben Martins, Limin Jia, Corina S. Păsăreanu | 19m |
Crabtree is a Rust API test synthesizer that combines program synthesis with fuzzing using a coverage- and type-guided DFS to grow tests and inputs; it… | ||
| QuAC: Quick Attribute-Centric Type Inference for Python | Jifeng Wu, Caroline Lemieux | 18m |
QuAC collects attribute sets for expressions, builds a class-query DB (builtins, stdlib protocols, imported and user classes), and ranks candidates with BM25… | ||
| On the Expressive Power of Languages for Static Variability | Paul Maximilian Bittner, Alexander Schultheiß, Benjamin Moosherr, Jeffrey M. Young, Leopoldo Teixeira, Eric Walkingshaw, Parisa Ataei, Thomas Thüm | 18m |
A formal semantic domain for static variability models configurations as functions-to-variants, and the paper proves soundness, completeness, and relative… | ||
| CoolerSpace: A Language for Physically Correct and Computationally Efficient Color(…) | Ethan Chen, Jiwon Chang, Yuhao Zhu | 17m |
A Python library that defines a domain-specific language for color physics, CoolerSpace uses a type-driven physical units type system to forbid mixing… | ||
| Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization | Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Lef Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, Andrew Wells | 20m |
Cedar defines a concise DSL, a Rust evaluation engine, and a Lean formal model that proves key properties; policies compile into SMT in the sound and complete… | ||
| Synthetiq: Fast and Versatile Quantum Circuit Synthesis | Anouk Paradis, Jasper Dekoninck, Benjamin Bichsel, Martin Vechev | 20m |
Synthetiq uses Simulated Annealing with a domain-specific energy function and a custom simplification pass to synthesize circuits over arbitrary finite gate… | ||
| Quarl: A Learning-Based Quantum Circuit Optimizer | Zikun Li, Jinjun Peng, Yixuan Mei, Sina Lin, Yi Wu, Oded Padon, Zhihao Jia | 19m |
Quarl is a reinforcement-learning quantum circuit optimizer that replaces greedy search with a policy trained via PPO, decomposes millions of actions into a… | ||
| Quantum Probabilistic Model Checking for Time-Bounded Properties | Seungmin Jeon, Kyeongmin Cho, Chan Gu Kang, Janggun Lee, Hakjoo Oh, Jeehoon Kang | 18m |
Encodes time-bounded probabilistic model checking as quantum circuits that superpose the 2^n state distribution, implements state transition circuits by… | ||
| Scenario-based Proofs for Concurrent Objects | Constantin Enea, Eric Koskinen | 19m |
Defines a small set of representative interleavings — the commutativity quotient — and an expression language (regular/context-free) that encodes them so… | ||
| Verified Lock-Free Session Channels with Linking | Thomas Somers, Robbert Krebbers | 16m |
Claims a verified lock-free implementation of asynchronous, bidirectional session channels (with per-direction buffers and a link/forward operation), proved… | ||
| Automated Robustness Verification of Concurrent Data Structure Libraries Against(…) | Kartik Nagar, Anmol Sahoo, Romit Roy Chowdhury, Suresh Jagannathan | 21m |
An automated procedure verifies that C11-style concurrent data-structure implementations are robust by checking that every relaxed-memory execution is possible… | ||
| Automated Verification of Parametric Channel-Based Process Communication | Georgian-Vlad Saioc, Julien Lange, Anders Møller | 16m |
A toolchain named Ginger translates Go fragments into a compact core language Virgo, encodes them as Hoare triples and checks partial-deadlock freedom using… | ||
| Concurrent Data Structures Made Easy | Callista Le, Kiran Gopinathan, Lee Koon Wen, Seth Gilbert, Ilya Sergey | 19m |
Library named OBatcher implements implicit batching in Multicore OCaml using async/await and functors; implicit-batching core is ~230 LOC, each generic… | ||
| WhiteFox: White-box Compiler Fuzzing Empowered by Large Language Models | Chenyuan Yang, Yinlin Deng, Runyu Lu, Jiayi Yao, Jiawei Liu, Reyhaneh Jabbarvand, Lingming Zhang | 19m |
WhiteFox is a white‑box compiler fuzzer that reads optimization source code, uses an analysis agent (GPT‑4) to summarize the precise triggering requirements… | ||
| Statically Contextualizing Large Language Models with Typed Holes | Andrew Blinn, Xiang Li, June Hyung Kim, Cyrus Omar | 20m |
Integration of a typed live editor with LLM completions produces fewer hallucinations by sending a Hazel language server–constructed static slice: inferred… | ||
| Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs | Federico Cassano, John Gouwar, Francesca Lucchetti, Claire Schlesinger, Anders Freeman, Carolyn Jane Anderson, Molly Q Feldman, Michael Greenberg, Abhinav Jangda, Arjun Guha | 20m |
Presents MultiPL-T, a pipeline that generates semi‑synthetic training data by using a Code LLM to synthesize unit tests for 130K vetted Python functions… | ||
| Evaluating the effectiveness of Deep Learning Models for Foundational Program Analysis(…) | Qian Chen, Chenyang Yu, Ruyan Liu, Chi Zhang, Yu Wang, Ke Wang, Ting Su, Linzhang Wang | 18m |
Compares CuBERT, CodeBERT, GGNN and Graph Sandwiches on two concrete tasks—alias prediction (must/may/must-not) and semantic equivalence—using a new CodeSem… | ||
| When Your Infrastructure is a Buggy Program: Understanding Faults in Infrastructure as(…) | Georgios-Petros Drosos, Thodoris Sotiropoulos, Georgios Alexopoulos, Dimitris Mitropoulos, Zhendong Su | 20m |
360 bugs across Ansible Puppet Chef registries are analyzed and classified into six symptom groups (most commonly external configuration failures), ten root… | ||
| Wasm-R3: Record-Reduce-Replay for Realistic and Standalone WebAssembly Benchmarks | Doehyun Baek, Jakob Getz, Yusung Sim, Daniel Lehmann, Ben L. Titzer, Sukyoung Ryu, Michael Pradel | 17m |
Builds bytecode instrumentation that record-reduce-replays Wasm executions, uses a shadow memory optimization plus call-state filtering to shrink traces from… | ||
| Iterative-Epoch Online Cycle Elimination for Context-Free Language Reachability | Pei Xu, Yuxiang Lei, Yulei Sui, Jingling Xue | 17m |
An iterative-epoch framework identifies grammar transitive symbols and collapses on-the-fly cycles in CFL-reachability graphs, reducing worklist blowup and… | ||
| Dependency-aware Code Naturalness | Chen Yang, Junjie Chen, Jiajun Jiang, Yuliang Huang | 22m |
Proposes DAN that builds a program dependency graph, extracts DFS paths then fixed-length subpaths, and measures sequence-level naturalness with n‑gram and… | ||
| AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects | Wolf Honore, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Zhong Shao | 18m |
Claims a single abstraction, AdoB abstraction, unifies benign and Byzantine consensus and lets proofs be done by refinement; implements it in Coq with… | ||
| VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity(…) | Yang He, Pinhan Zhao, Xinyu Wang, Yuepeng Wang | 20m |
VeriEQL encodes SQL semantics over symbolic tuples using an SMT encoding with integers and uninterpreted functions and checks bounded equivalence by… | ||
| Seneca: Taint-Based Call Graph Construction for Java Object Deserialization | Joanna C. S. Santos, Mehdi Mirakhorli, Ali Shokri | 19m |
Seneca implements a two-phase, taint-driven extension to call-graph construction that inserts synthetic serialization methods and uses taint-state propagation… | ||
| Semantic-Type-Guided Bug Finding | Kelvin Qian, Scott F. Smith, Brandon Stride, Shiwei Weng, Ke Wu | 18m |
Introduces a semantic-type refuter that is co-recursively enumerable and proves soundness and completeness against a semantic model; implements the checker and… | ||
| Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach | Haonan Li, Yu Hao, Yizhuo Zhai, Zhiyun Qian | 18m |
A framework called LLift combines an existing static checker (UBTag) with iterative LLM queries to resolve UBTag’s 53k “undecided” paths, using post-constraint… | ||
| Quantum Control Machine: The Limits of Control Flow in Quantum Programming | Charles Yuan, Agnes Villanyi, Michael Carbin | 24m |
Proves that a straightforward conditional jump impossibility holds: lifting classical conditional jumps into superposition is nonrealizable, with a formal… | ||
| Non-Termination Proving at Scale | Azalea Raad, Julien Vanegue, Peter W. O'Hearn | 19m |
Claims a sound and complete under-approximate logic called UNTerSL that composes incorrectness/divergence reasoning with separation logic and bi-abduction to… | ||
| Newtonian Program Analysis of Probabilistic Programs | Di Wang, Thomas Reps | 20m |
Presents NPA-PMA, an interprocedural framework that generalizes Newtonian Program Analysis to probabilistic, nondeterministic, and conditional branching by… | ||
| MEA2: a Lightweight Field-Sensitive Escape Analysis with Points-to Calculation for Golang | Boyao Ding, Qingwei Li, Yu Zhang, Fugen Tang, Jinbao Chen | 22m |
MEA2 implements a field-sensitive escape analysis with points-to calculation on top of the GoLLVM/GoRVM pipeline, adds a generic function-summary format for… | ||
| HardTaint: Production-Run Dynamic Taint Analysis via Selective Hardware Tracing | Yiyu Zhang, Tianyi Liu, Yueyang Wang, Yun Qi, Kai Ji, Jian Tang, Xiaoliang Wang, Xuandong Li, Zhiqiang Zuo | 16m |
System builds a production-capable dynamic taint pipeline by statically identifying minimal trace points, rewriting binaries to emit only those values via… | ||
| Sound and partially-complete static analysis of data-races in GPU programs | Dennis Liew, Tiago Cogumbreiro, Julien Lange | 15m |
A sound static verifier and a partially-complete race finder named FaialAA implements memory-access protocols, SMT encoding, and mechanized proofs to guarantee… | ||
| ParDiff: Practical Static Differential Analysis of Network Protocol Parsers | Mingwei Zheng, Qingkai Shi, Xuwei Liu, Xiangzhe Xu, Le Yu, Congyu Liu, Guannan Wei, Xiangyu Zhang | 21m |
ParDiff statically extracts protocol-format constraints from C implementations, extracts finite-state machines ordered by buffer indices, and uses bisimulation… | ||
| FlowCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic(…) | Zhengyao Lin, Joshua Gancher, Bryan Parno | 21m |
FlowCert implements translation validation from LLVM to asynchronous dataflow graphs for the RipTide CGRA by constructing a deterministic canonical schedule… | ||
| Computing Precise Control Interface Specifications | Eric Hayden Campbell, Hossein Hojjat, Nate Foster | 19m |
Algorithm computes precise control interface specs for data-plane programs by lifting GCL programs, applying quantifier elimination, and using a path-based… | ||
| Cocoon: Static Information Flow Control in Rust | Ada Lamba, Max Taylor, Vincent Beardsley, Jacob Bambeck, Michael D. Bond, Zhiqiang Lin | 18m |
Cocoon is a Rust library that enforces noninterference by using Rust’s type system and procedural macros to create a type-and-effect IFC system without… | ||
| StarMalloc: Verifying a Modern, Hardened Memory Allocator | Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko | 19m |
StarMalloc is a verified, concurrent, hardened user-space allocator implemented in F/Steel, extracted to C and proven functionally correct relative to a… | ||
| Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA(…) | Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, Azalea Raad | 18m |
Claims a first formal semantics for RDMA on x86‑TSO: three equivalent models (two operational at different abstraction levels, one declarative), with a… | ||
| PROMPT: A Fast and Extensible Memory Profiling Framework | Ziyang Xu, Yebin Chon, Yian Su, Zujun Tan, Sotiris Apostolakis, Simone Campanoni, David I. August | 19m |
A framework that standardizes instrumentation and decouples event generation from analysis, PROMPT implements shared shadow memory, context management… | ||
| A Runtime System for Interruptible Query Processing – When Incremental Computing Meets(…) | Jeffrey Eymer, Philip Dexter, Joseph Raskind, Yu David Liu | 19m |
Pitstop implements interruptible query processing by partitioning graphs into legs with pit stops, letting queries pause and resume at fine-grained boundaries… | ||
| Making Sense of Multi-Threaded Application Performance at Scale with NonSequitur | Augustine Wong, Paul Bucci, Ivan Beschastnikh, Alexandra Fedorova | 19m |
NonSequitur compresses multi‑threaded traces with a domain‑specific merge of identical call stacks, leaves long events uncompressed so latency spikes remain… | ||
| Validating SMT Solvers for Correctness and Performance via Grammar-based Enumeration | Dominik Winterer, Zhendong Su | 21m |
ET is a grammar-based enumerator that compiles eight SMT theory grammars into algebraic datatypes and drives the FEAT enumerator to produce smallest-to-largest… | ||
| SMT2Test: From SMT Formulas to Effective Test Cases | Chengyu Zhang, Zhendong Su | 18m |
SMT2Test transforms SMT formulas into executable programs (Dafny and C via an intermediate representation) and encodes satisfiability as a reachability… | ||
| Hypra: A Deductive Program Verifier for Hyper Hoare Logic | Thibault Dardinier, Anqi Li, Peter Müller | 22m |
Claims the first automated deductive technique for arbitrary hyperproperties by encoding sets of program states explicitly into an intermediate language and… | ||
| Compositionality and Observational Refinement for Linearizability with Crashes | Arthur Oliveira Vale, Zhongye Wang, Yixuan Chen, Peixin You, Zhong Shao | 12m |
Defines a compositional model for full-system crashes and proves that a new criterion, crash-aware linearizability, supports both locality and observational… | ||
| Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…) | Shaan Nagy, Jinwoo Kim, Thomas Reps, Loris D'Antoni | 20m |
Presents Wuldo, the first implementation of an Unrealizability Logic (UL) proof synthesizer that decouples a fixed proof skeleton from parametric nonterminal… | ||
| Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…) | Maxime Legoupil, June Rousseau, Aina Linn Georges, Jean Pichon-Pharabod, Lars Birkedal | 21m |
Mechanisation produces MSWasmCert as a conservative, proof‑assistant formalisation of MSWasm and WebAssembly 1.0 modules, and builds Iris‑MSWasm: a separation… | ||
| Mark–Scavenge: Waiting for Trash to Take Itself Out | Jonas Norlinder, Erik Österlund, David Black-Schaffer, Tobias Wrigstad | 21m |
Implements MS-ZGC on OpenJDK that delays evacuation and only scavenges previously selected sparse pages, using just-in-time evacuations to avoid OOM. Compares… | ||
| A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code | Julien Simonnet, Matthieu Lemerre, Mihaela Sighireanu | 19m |
A dependent nominal physical type system called Typed C models contiguous memory regions with nesting, unions and mild update semantics to express pointer… | ||
| Learning Abstraction Selection for Bayesian Program Analysis | Yifan Zhang, Yuanfeng Shi, Xin Zhang | 18m |
Framework learns which abstraction parameters to change by extracting derivation graphs before and after a candidate refinement, computing graph features… | ||
| Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security(…) | Martin Avanzini, Gilles Barthe, Benjamin Gregoire, Georg Moser, Gabriele Vanoni | 18m |
Proposes a EHL + pRHL hopping rule that reduces expectation-based proof goals to related programs, implements it inside EasyCrypt integration, and proves… | ||
| Exact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions | Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen | 24m |
Claims exact Bayesian posteriors for probabilistic programs with unbounded loops and conditioning by giving a denotational semantics based on extended… | ||
| Distributions for Compositionally Differentiating Parametric Discontinuities | Jesse Michel, Kevin Mu, Xuanda Yang, Sai Praveen Bangaru, Elias Rojas Collins, Gilbert Louis Bernstein, Jonathan Ragan-Kelley, Michael Carbin, Tzu-Mao Li | 23m |
Introduces Potto prototype as the first differentiable first-order language that soundly differentiates parametric discontinuities, gives a denotational… | ||
| A modal type-theory of expected cost in higher-order probabilistic programs | Vineet Rajani, Gilles Barthe, Deepak Garg | 18m |
pλ-amor is a graded modal type theory that encodes probabilities, potentials and expected cost at the type level and proves bounds for higher-order… | ||
| Understanding and Finding Java Decompiler Bugs | Yifei Lu, Weidong Hou, Minxue Pan, Xuandong Li, Zhendong Su | 21m |
Systematic study of 333 real bug reports identifies that 40.2% have small repro tests, over 80% manifest as exceptions, syntactic, or semantic errors, and the… | ||
| SparseAuto: An Auto-Scheduler for Sparse Tensor Computations Using Recursive Loop Nest(…) | Adhitha Dias, Logan Anderson, Kirshanthan Sundararajah, Artem Pelenitsyn, Milind Kulkarni | 20m |
SparseAuto is an auto-scheduler that applies recursive loop-nest fission/fusion to produce imperfectly nested code, uses a poset-based cost model combining… | ||
| PolyJuice: Detecting Mis-Compilation Bugs in Tensor Compilers with Equality Saturation(…) | Chijin Zhou, Bingzhou Qian, Gwihwan Go, Quan Zhang, Shanshan Li, Yu Jiang | 19m |
PolyJuice builds equivalent tensor-graph variants via equality saturation and selects the most simplified and most complex extracts to force different… | ||
| Minotaur: A SIMD-Oriented Synthesizing Superoptimizer | Zhengyang Liu, Stefan Mada, John Regehr | 19m |
Minotaur is a synthesizing superoptimizer for LLVM that searches SSA cuts and enumerates cheaper SIMD and scalar rewrites then formally verifies them with… | ||
| Hydra: Generalizing Peephole Optimizations with Program Synthesis | Manasij Mukherjee, John Regehr | 19m |
Hydra uses program synthesis to turn specific superoptimizer rewrites into width-independent rules by synthesizing symbolic constants, dataflow preconditions… | ||
| Homeostasis: Design and Implementation of a Self-Stabilizing Compiler (TOPLAS) | Aman Nougrahiya, V Krishna Nandivada | 20m |
Homeostasis is a compiler framework that automatically captures program changes into a centralized compressed log, triggers stabilization on demand, and… | ||
| Fully Verified Instruction Scheduling | Ziteng Yang, Jun Shirako, Vivek Sarkar | 19m |
Claims a first mechanized library for fully verified instruction scheduling that proves any scheduler correct by reducing proofs to one local transformation… | ||
| Compiling Recurrences over Dense and Sparse Arrays | Shiv Sundram, Muhammad Usman Tariq, Fredrik Kjolstad | 19m |
A compiler framework that takes recurrence equations, data-format declarations, and schedule commands and emits native C for dense and sparse arrays by… | ||
| Compiler Support for Sparse Tensor Convolutions | Peiming Liu, Alexander J Root, Anlun Xu, Yinying Li, Fredrik Kjolstad, Aart Bik | 19m |
Compiler extends sparse tensor algebra compilation to handle affine subscripts by rewriting compound indices into loop-driven subsection iterators and five… | ||
| Compilation of Shape Operators on Sparse Arrays | Alexander J Root, Bobby Yan, Peiming Liu, Christophe Gyurgyik, Aart Bik, Fredrik Kjolstad | 18m |
A compiler called burrito extends the taco compiler to emit specialized C++ iterators that traverse reshaped sparse formats without materializing temporaries… | ||
| Message-Observing Sessions | Ryan Kavanagh, Brigitte Pientka | 20m |
Most is a process language that adds message-observing session types — a restricted form of type-level computation — to binary session types so protocols on… | ||
| Inductive diagrams for causal reasoning | Jonathan Castello, Patrick Redmond, Lindsey Kuper | 20m |
Defines causal separation diagrams as an inductive, diagrammatic syntax that makes impossible executions unrepresentable and enforces consistent cuts, then… | ||
| Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping(…) | Wenjia Ye, Yaozhu Sun | 20m |
The paper shows that by restricting the typing rule for references (rather than dropping distributivity or adding a global value restriction) bidirectional… | ||
| A Constraint Solving Approach to Parikh Images of Regular Languages | Amanda Stjerna, Philipp Rümmer | 19m |
Presents a constraint-solving reframing of Parikh-image extraction: build PC calculus and a standalone tool Catra tool* that ties to the Princess SMT engine… | ||
| Weighted Context-Free-Language Ordered Binary Decision Diagrams | Meghana Aparna Sistla, Swarat Chaudhuri, Thomas Reps | 21m |
Introduces WCFLOBDDs, a hierarchically structured, weighted BDD with a procedure-call mechanism that is canonical and supports polynomial-time operations… | ||
| VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts | Yichuan Li, Wei Song, Jeff Huang | 19m |
VarLifter recovers typed state variables from Solidity bytecode by treating every accessed field as a candidate variable, pruning false positives, then… | ||
| Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…) | Noam Zilberstein, Angelina Saliling, Alexandra Silva | 21m |
Outcome Separation Logic gives a single formalism that proves both correctness and incorrectness for programs with effects by making postconditions talk about… | ||
| AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming | Robert Schenck, Nikolaj Hey Hinnerskov, Troels Henriksen, Magnus Madsen, Martin Elsman | 20m |
Automatic insertion of maps and replicates makes rank-polymorphic calls type-check by encoding per-application rank choices as integer variables and solving a… | ||
| Realistic Realizability: Specifying ABIs You Can Count On | Andrew Wagner, Zachary Eisbach, Amal Ahmed | 19m |
Proposes using realistic realizability models to specify ABIs by connecting high-level types to concrete target code and builds a graph-based separation logic… | ||
| Synthesizing Formal Semantics from Executable Interpreters | Jiangyi Liu, Charlie Murphy, Anvay Grover, Keith J.C. Johnson, Thomas Reps, Loris D'Antoni | 21m |
Given a grammar and a closed-box interpreter the system Synantic synthesizes inductive, syntax-directed semantics as Constrained-Horn Clauses via a CEGIS loop… | ||
| Semantics Lifting for Syntactic Sugar | Zhichao Guan, Yiyuan Cao, Tailai Yu, Ziheng Wang, Di Wang, Zhenjiang Hu | 18m |
Presents an algorithm that derives host-independent evaluation rules from host semantics and desugaring rules and implements it as Osazone, a tool that lifts… | ||
| HOL4P4: mechanized small-step semantics for P4 | Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam | 19m |
Claims a first complete P416 semantics that models extern-concurrency interactions and captures pipelines end-to-end, formalized in HOL4 with a heapless… | ||
| Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…) | Keith J.C. Johnson, Rahul Krishnan, Thomas Reps, Loris D'Antoni | 20m |
Claims that monotonicity of concrete semantics lets an SMT solver automatically generate sound and often tight interval abstractions for top‑down enumerative… | ||
| A Pure Demand Operational Semantics with Applications to Program Analysis | Scott F. Smith, Robert Zhang | 19m |
Defines an operational semantics whose entire machine state is just a call stack plus a source program point or lexical depth, with no environment or… | ||
| nothing matches | ||