OOPSLA 2025
2025-10-16..2025-10-18
Singapore, Singapore
OOPSLA ·
[OOPSLA 2018, OOPSLA 2020, OOPSLA 2021, OOPSLA 2022, OOPSLA 2023, OOPSLA 2024, OOPSLA 2025]
| title | author | length |
|---|---|---|
| Language-Parametric Reference Synthesis | Daniel A. A. Pelsmaeker, Aron Zwaan, Casper Bach, Arjan J. Mooij | 15m |
Automated refactoring preserves original declaration targets by replacing references with locked references during transformation and synthesizing concrete… | ||
| Structural Information Flow: A Fresh Look at Types for Non-Interference | Hemant Gouni, Frank Pfenning, Jonathan Aldrich | 15m |
Type system separates data abstraction from information flow, turns single labels into dependency sets, and encodes quantifiers as existentials so module… | ||
| Products of Recursive Programs for Hypersafety Verification | Ruotong Cheng, Azadeh Farzan | 15m |
Proposes an algorithmic construction of an infinite family of product programs that reduce hypersafety of recursive programs to ordinary safety, using visibly… | ||
| Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials | Qihao Lian, Di Wang | 14m |
Claims an automatic, type-based AARA for Rust that infers symbolic linear cost bounds and proves soundness via a new Resource-Aware Borrow Calculus (RABC)… | ||
| Universal Scalability in Declarative Program Analysis (with Choice-Based Combination(…) | Anastasios Antoniadis, Ilias Tsatiris, Neville Grech, Yannis Smaragdakis | 15m |
Uses the choice construct in Souffle to enforce multiplicity bounds by hashing an extra index field, letting relations be pruned when a projected key exceeds a… | ||
| Compositional Quantum Control Flow with Efficient Compilation in Qunity | Mikhail Mints, Finn Voichick, Leonidas Lampropoulos, Robert Rand | 15m |
Implementation of the first Qunity compiler that lowers high-level quantum control into OpenQASM 3 and a set of concrete optimizations. Adds two control… | ||
| A Language for Quantifying Quantum Network Behavior | Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Soulé, Robert Rand, Patrick Eugster | 14m |
A domain specific language called PBKAT models Bell pair distribution with probabilistic actions (e.g. create succeeds 0.81, swap 0.6) plus nondeterministic… | ||
| Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits | Junrui Liu, Jiaxin Song, Yanning Chen, Hanzhi Liu, Hongbo Wen, Luke Pearson, Yanju Chen, Yu Feng | 15m |
Tabby is a compiler that converts high-level ZK programs into optimized arithmetic circuits by lowering to a domain-specific IR, decomposing the dataflow into… | ||
| Efficient Decrease-And-Conquer Linearizability Monitoring | Zheng Han Lee, Umang Mathur | 10m |
Presents a decrease-and-conquer framework that reduces linearizability monitoring to finding linearizability-preserving values, proving polynomial-time… | ||
| Compositional Symbolic Execution for the Next 700 Memory Models | Andreas Lööw, Seung Hoon Park, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Opale Sjöstedt, Philippa Gardner | 16m |
Presents a mechanized formal foundation for memory-model‑parametric compositional symbolic execution, claiming soundness for both separation logic and… | ||
| A Unifying Approach to Product Constructions for Quantitative Temporal Inference | Kazuki Watanabe, Sebastian Junges, Jurriaan Rot, Ichiro Hasuo | 14m |
Presents a categorical recipe that turns a system and a temporal specification into a product via coalgebraic modelling and a natural distributive law, then… | ||
| Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path(…) | Matteo Basso, Aleksandar Prokopec, Andrea Rosà, Walter Binder | 14m |
Proposes CAHP (context-augmented heap paths) and a prefix-tree based exact and partial path matching pipeline, integrated into GraalVM Native Image to remap… | ||
| The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with(…) | Jiří Beneš, Jonathan Immanuel Brachthäuser | 15m |
Claims that overloads are representable as explicit choices so constraint collection, solving, and resolution stay separate, using a flow-based variational… | ||
| The Continuous Tensor Abstraction: Where Indices are Real | Jaeyeon Won, Willow Ahrens, Teodoro F. Collin, Joel S Emer, Saman Amarasinghe | 16m |
Introduces a compiler and code generator that lets tensor indices be real numbers and represents data as piecewise-constant tensors so infinite domains execute… | ||
| Statically Analyzing the Dataflow of R Programs | Florian Sihler, Matthias Tichy | 15m |
Presents a novel static dataflow analysis for R that handles dynamic scoping, lazy evaluation with side effects, and reflective redefinitions and produces a… | ||
| Hambazi: Spatial Coordination Synthesis for Augmented Reality | Yi-Zhen Tsai, Jiasi Chen, Mohsen Lesani | 15m |
HAMBAZI implements well-organized replicated data types for multi-user AR using an escrow-style credit scheme plus a replication protocol and an SMT solver… | ||
| Notions of Stack-manipulating Computation and Relative Monads | Yuchen Jiang, Runze Xue, Max S. New | 17m |
Adapts the category-theoretic notion of relative monads to a polymorphic call-by-push-value calculus to model concrete stack-based implementations of effects… | ||
| ABC: Towards a Universal Code Styler through Model Merging | Yitong Chen, Zhiqiang Gao, Chuanqi Shi, Baixuan Li, Miao Gao | 14m |
Proposes merging many small fine-tuned code LMs into one styler: train per-criterion basis models (0.5B, 1.3B, 1.5B, 3B), then apply a four-step Clip and… | ||
| Incremental Bidirectional Typing via Order Maintenance | Thomas J. Porter, Marisa Kirisame, Ivan Wei, Pavel Panchekha, Cyrus Omar | 14m |
Presents a small-step incremental bidirectional type system that maintains binding pointers with an order maintenance data structure so inserts/deletes and… | ||
| Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of(…) | Yumeng He, Chandrakana Nandi, Sreepathi Pai | 15m |
Formalizes G‑code as sets of cuboids then samples them into point clouds and implements an efficient differential checker called GlitchFinder; prototype… | ||
| Dependency-Aware Compilation for Surface Code Quantum Architectures | Abtin Molavi, Amanda Xu, Swamit Tannu, Aws Albarghouthi | 14m |
Presents a compiler that maps logical qubits to a 2D surface‑code grid using a layered interaction graph to expose only the operations that can conflict, then… | ||
| Dynamic Wind for Effect Handlers | David Voigt, Philipp Schuster, Jonathan Immanuel Brachthäuser | 14m |
Adds three handler clauses (on suspend, on resume, on return) to lexical effect handlers and formalizes semantics and a type system that make multi‑shot… | ||
| MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming | Jayanaka Dantanarayana, Yiping Kang, Kugesan Sivasothynathan, Christopher Clarke, Baichuan Li, Savini Kashmira, Krisztian Flautner, Lingjia Tang, Jason Mars | 16m |
Presents MTP, a language-level way to call LLMs that adds a by operator and a runtime pipeline that extracts code semantics into MT-IR and drives an automated… | ||
| Checking $\delta$-Satisfiability of Reals with Integrals | Cody Rivera, Bishnu Bhusal, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan | 13m |
Extends δ-decision procedures to handle integrals by implementing ∫dReal on top of dReal and combining IBEX interval propagation with the ARB… | ||
| Contract System Metatheories à la Carte: A Transition-System View of Contracts | Shu-Hung You, Christos Dimoulas, Robert Bruce Findler | 15m |
Models higher-order contracts as a parameterized transition system and proves that composing annotations and registers yields reusable metatheory: ownership… | ||
| Interactive Bit Vector Reasoning using Verified Bitblasting | Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex Keizer, Léon Frenot, Abdalrhman Mohamed, Leo Stefanesco, Harun Khan, Joshua Clune, Clark Barrett, Tobias Grosser | 13m |
A verified bit-blasting pipeline called bv_decide tactic compiles Lean bitvector goals to AIGs, converts to CNF, calls an external SAT solver that emits… | ||
| From Linearity to Borrowing | Andrew Wagner, Olek Gierczak, Brianna Marshall, John M. Li, Amal Ahmed | 16m |
Builds a lightweight borrowing extension on a linear lambda calculus and implements the API as untyped terms validated by logic, not new runtime primitives… | ||
| Modular Reasoning about Global Variables and Their Initialization | João Pereira, Isaac van Bakel, Patricia Firlejczyk, Marco Eilers, Peter Müller | 15m |
Presents a verification method that lets clients assume global state only when three concrete conditions hold: module invariants are established… | ||
| On Abstraction Refinement for Bayesian Program Analysis | Yuanfeng Shi, Yifan Zhang, Xin Zhang | 15m |
Paper proposes an online abstraction search called BSRefine that performs counterexample-guided refinement on Bayesian program analyses by cutting information… | ||
| Shaking Up Quantum Simulators with Fuzzing and Rigour | Vasileios Klimis, Karine Even-Mendoza, Avner Bensoussan, Elena Chachkarova, Sophie Fortz, Connor Lenihan | 19m |
FuzzQ combines an Alloy-based QASM 3.0 model with structured fuzzing, mutation testing and invariant checks to generate constraint-guided circuits and run… | ||
| Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations | Yi Zhang, Yu Wang, Linzhang Wang, Ke Wang | 14m |
Synchronized Behavior Checking cross-validates pairs of optimizations by mutating programs and checking co-occurring and complementary coordinated behaviors so… | ||
| MIO: Multiverse Debugging in the face of Input/Output | Tom Lauwaerts, Maarten Steevens, Christophe Scholliers | 14m |
Prototype MIO runs on the WARDuino WebAssembly VM on STM32 microcontrollers and lets developers mock sensor reads, jump between branches by restoring the… | ||
| CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers | Aditya Anand, Vijay Sundaresan, Daryl Maier, Manas Thakur | 14m |
CoSSJIT generates polymorphic conditions, branching conditions, and inlining conditions during a static interprocedural dataflow analysis and feeds those… | ||
| GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler | Damitha Lenadora, Nikhil Jayakumar, Chamika Sudusinghe, Charith Mendis | 15m |
GALA is a domain-specific language and compiler that composes intra-operator scheduling commands with automatic inter-operator rewrites via two novel IRs, a… | ||
| Scalable Equivalence Checking and Verification of Shallow Quantum Circuits | Nengkun Yu, Xuan Du Trinh, Thomas Reps | 15m |
Projection-Based Equivalence Checking constructs a constraint representation of a shallow circuit’s output as a conjunction of local projections that act on… | ||
| Memory-Safety Verification of Open Programs With Angelic Assumptions | Gourav Takhar, Baldip Bijlani, Prantik Chatterjee, Akash Lal, Subhajit Roy | 12m |
Seeker automatically suppresses spurious memory-safety warnings in open C programs by mining 1,900+ buffer idioms from an LLM, collapsing them into seven… | ||
| On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs | Taro Sekiyama, Ugo Dal Lago, Hiroshi Unno | 14m |
Claims decidability for a nontrivial fragment of effectful higher-order programs by introducing polymorphic answer-type □ and a type system that allows… | ||
| Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice | Jay Richards, Daniel Wright, Simon Cooksey, Mark Batty | 15m |
Claims a thin-air free memory model that justifies every write with a symbolic justification structure (control/data dependencies plus elaborations) so… | ||
| A Flow-Sensitive Refinement Type System for Verifying eBPF Programs | Ameer Hamza, Lucas Zavalia, Arie Gurfinkel, Jorge A. Navas, Grigory Fedyukovich | 14m |
Type-based verifier infers proof certificates in userspace and pushes only a small checker into the kernel, reducing the trusted codebase. Implementation… | ||
| REPTILE: Performant Tiling of Recurrences | Muhammad Usman Tariq, Shiv Sundram, Fredrik Kjolstad | 15m |
REPTILE is a compiler that tiles mathematical recurrences by decomposing programs into unique hierarchical tiles, simplifying each tile into its own… | ||
| Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations | Zhenyang Xu, Yongqiang Tian, Mengxiao Zhang, Chengnian Sun | 15m |
Introduces Structure Form Conversion as a new syntax-guided transformation and implements three methods including Smaller Structure Replacement and Structure… | ||
| Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE(…) | Jacob Laurel, Ignacio Laguna, Jan Hueckelheim | 14m |
Phocus synthesizes sound, precise abstract transformers for Lax‑Friedrichs, Leapfrog and Upwind finite difference schemes by finding a best linear… | ||
| PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns | Donguk Kim, Doha Hwang, Minseok Jeon, Hakjoo Oh | 15m |
PAFL mines project histories to synthesize project-specific fault patterns and boosts existing fault localizers by reweighting statement suspiciousness. It… | ||
| On the Impact of Formal Verification on Software Development | Eric Mugnier, Zhou Yuanyuan, Ranjit Jhala, Michael Coblenz | 15m |
Auto-active verifier Dafny is studied via 14 interviews using grounded theory and the paper reports concrete pain points: SMT queries balloon to 5 GB of SMT… | ||
| Tuning Random Generators: Property-Based Testing as Probabilistic Programming | Ryan Tjoa, Poorva Garg, Harrison Goldstein, Todd Millstein, Benjamin C. Pierce, Guy Van den Broeck | 15m |
Generators become probabilistic programs with symbolic weights and are tuned by computing a symbolic distribution, compiling it into compressed BDD-based… | ||
| Scaling Optimization Over Uncertainty via Compilation | Minsung Cho, John Gouwar, Steven Holtzen | 15m |
Presents a compilation pipeline that turns loop-free probabilistic programs into a new IR — binary decision diagrams weighted by a branch-and-bound semiring —… | ||
| Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for(…) | Ross Tate | 15m |
First sound and complete decision procedure for validating nominal object oriented programs with generic interfaces that are irregularly recursive without… | ||
| Abstract Interpretation of Temporal Safety Effects of Higher Order Programs | Mihai Nicola, Chaitanya Agarwal, Eric Koskinen, Thomas Wies | 15m |
Introduces an abstract effect domain that summarizes context‑sensitive dependent effects as symbolic automata with accumulators, gives an abstract transformer… | ||
| Bennet: Randomized Specification Testing for Heap-Manipulating Programs | Zain K Aamer, Benjamin C. Pierce | 15m |
Bennet synthesizes C test generators from CN specifications by compiling preconditions into a DSL and running randomized backtracking search to place heap… | ||
| Synthesizing DSLs for Few-Shot Learning | Paul Krogmeier, P. Madhusudan | 15m |
Constructs a precise formulation: given a base language L, a complexity measure (parse tree depth), and a metagrammar of candidate DSLs, decides whether a… | ||
| Liberating Merges via Apartness and Guarded Subtyping | Han Xu, Xuejing Huang | 15m |
Introduces type apartness plus a strengthened guarded subtyping that lets merges overlap yet remain deterministic, enabling function and return-type… | ||
| Compressed and Parallelized Structured Tensor Algebra | Mahdi Ghorbani, Emilien Bauer, Tobias Grosser, Amir Shaikhha | 14m |
DASTAC generates compressed linear indexes from polyhedral structure using the Barvinok algorithm, emits affine code and parallel loops via MLIR, and adds… | ||
| Multi-Language Probabilistic Programming | Sam Stites, John Li, Steven Holtzen | 14m |
Introduces MultiPPL, a multi-language that stitches an exact-discrete engine (DICE / BDD knowledge compilation) to an approximate sampler (K with importance… | ||
| Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal(…) | Anan Kabaha, Dana Drachsler Cohen | 14m |
Claims a practical verifier, LUCID, that computes an iDP-DB overapproximation so noise is added only to inputs that actually risk leaking labels; it encodes… | ||
| Choreographic Quick Changes: First-Class Location (Set) Polymorphism | Ashley Samuelson, Andrew K. Hirsch, Ethan Cecchetti | 11m |
A new choreographic language, λQC, adds first-class process names and polymorphism over types and sets of locations, plus algebraic and recursive data types… | ||
| Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive(…) | Chaoyue Zhang, Longlong Lu, Yifei Lu, Minxue Pan, Xuandong Li | 15m |
A practical selective object-sensitive pointer-analysis framework named Moon identifies which heap objects actually improve precision by reducing the problem… | ||
| Fuzzing C++ Compilers via Type-Driven Mutation | Bo Wang, Chong Chen, Ming Deng, Junjie Chen, Xing Zhang, Youfang Lin, Dan Hao, Jun Sun | 14m |
TyMut is a mutation-based C++ type-system fuzzer that runs for 32 hours to generate and test 250,584 programs, using 30 mutation operators across five… | ||
| Artemis: Toward Accurate Detection of Server-Side Request Forgeries through(…) | Yuchen Ji, Ting Dai, Zhichao Zhou, Yutian Tang, Jingzhu He | 15m |
Artemis implements an LLM-assisted interprocedural, path-sensitive taint analysis for PHP that builds explicit and implicit call graphs (including magic… | ||
| Verification of Bit-Flip Attacks against Quantized Neural Networks | Yedi Zhang, Lei Huang, Pengfei Gao, Fu Song, Jun Sun, Jin Song Dong | 17m |
BFAVerifier formally checks quantized neural networks for bit‑flip attacks by combining a sound abstraction‑based reachability engine with an MILP fallback… | ||
| HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical(…) | Sirui Lu, Rastislav Bodík | 15m |
Framework implements component-based synthesis with SMT backends, adds hierarchical instruction-choice embedding, adaptive partitioning and unrealizability… | ||
| TraceLinking Implementations with their Verified Designs | Finn Hackett, Ivan Beschastnikh | 15m |
TraceLink automatically maps runtime traces from PGo-generated Go programs back to their TLA+ designs, uses vector clocks to record causal partial orders, and… | ||
| Garbage Collection for Rust: The Finalizer Frontier | Jacob Hughes, Laurence Tratt | 15m |
Alloy implements a conservative, retrofit tracing GC for Rust that reuses existing drop methods as finalizers where safe, using a compiler pass called… | ||
| Characterizing Implementability of Global Protocols with Infinite States and Data | Elaine Li, Felix Stutz, Thomas Wies, Damien Zufferey | 13m |
Provides a semantic characterization that reduces implementability of symbolic global protocols to (co)reachability checks per participant and a set of… | ||
| Modeling Reachability Types with Logical Relations -- Semantic Type Soundness,(…) | Yuyan Bao, Songlin Jia, Guannan Wei, Oliver Bračevac, Tiark Rompf | 14m |
Presents a formal logical-relations model for reachability types that augments standard relations with relational store typing to localize heap reasoning, and… | ||
| Model-guided Fuzzing of Distributed Systems | Ege Berkay Gulcan, Burcu Kulahcioglu Ozkan, Rupak Majumdar, Srinidhi Nagendra | 14m |
An implementation of a fuzzer for TLA+ models drives scheduler-controlled seed schedules into real systems, maps runtime events to model actions, and uses TLA+… | ||
| Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in(…) | Guanlin Chen, Ruyi Ji, Shuhao Zhang, Yingfei Xiong | 14m |
Claims a new multi-way intersection algorithm that directly intersects many small VSAs to avoid huge intermediate structures, plus a bottom-up intersection… | ||
| MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM(…) | Peng Yuan, Yan Liu, Jianxin Lai, Long Li, Tianxiang Sui, Linjie Xiao, Xiaojing Zhang, Qing Zhu, Jingling Xue | 14m |
MetaKernel: Enabling Efficient Encrypted Neural Network Inference through Unified MVM and Convolution (Video, OOPSLA2 2025)
Peng Yuan, Yan Liu, JianXin Lai… | ||
| Automated Verification of Soundness of DNN Certifiers | Avaljot Singh, Yasmin Chandini Sarita, Charith Mendis, Gagandeep Singh | 14m |
Automates soundness checks for abstract-interpretation DNN certifiers by encoding certifier specs in the ConstraintFlow DSL, translating networks to a symbolic… | ||
| Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern | Patrick Redmond, Jonathan Castello, Jose Calderon, Lindsey Kuper | 14m |
Formal semantics Core ECS models ECS state and schedules, proves a class of programs are deterministic-by-construction despite relaxed mutation ordering, and… | ||
| SPLASH Organisers Discussion and AMA | Alex Potanin, Shriram Krishnamurthi, Sukyoung Ryu | 01h 12m |
Conversation reports concrete, actionable changes and tradeoffs: SIGPLAN plans a SIGPLAN track for missed presentations across conferences in 2026, review… | ||
| Bolt-On Strong Consistency: Specification, Implementation, and Verification | Nicholas V. Lewchenko, Gowtham Kaki, Bor-Yuh Evan Chang | 14m |
Shows how consensus safety can be proved from local properties by implementing strong replication atop a causal weak store and verifying at the single-node… | ||
| Modal Abstractions for Virtualizing Memory Addresses | Ismail Kuru, Colin S. Gordon | 15m |
Introduces a modal assertion [r]P that ties assertions to a particular page‑table root and a definition of virtual points-to that splits page‑table traversal… | ||
| An Empirical Study of Bugs in the rustc Compiler | Zixi Liu, Yang Feng, Yunbo Ni, Shaohua Li, Xizhe Yin, Qingkai Shi, Baowen Xu, Zhendong Su | 14m |
Analysis of 301 rustc issues from 2022–2024 shows concrete fault patterns: about 30% root in the type system, ~15% in ownership, ~15% from MIR optimizations… | ||
| FO-Complete Program Verification for Heap Logics | Adithya Murali, Hrishikesh Balakrishnan, Aaron Councilman, P. Madhusudan | 12m |
Claims a practical verification pipeline that achieves FO-Complete reasoning for heap logics by designing two logics — frame logic (FL) and SL-FL — with… | ||
| Type-Preserving Flat Closure Optimization | Adam T. Geller, Sean Bocirnea, Chester Gould, Paulette Koronkevich, William J. Bowman | 11m |
Proposes a new Flat-Closure Calculus (FCC) that encodes the flat closure calling convention with singleton types so the projected code pointer is typechecked… | ||
| Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness | Dongjae Lee, Janggun Lee, Taeyoung Yoon, Minki Cho, Jeehoon Kang, Chung-Kil Hur | 15m |
Lilo is a higher-order concurrent separation logic that adds a promise mechanism to reason about liveness: threads record a promise list and must consume… | ||
| Denotational Foundations for Expected Cost Analysis | Pedro Henrique Azevedo de Amorim | 13m |
Introduces cert CBPV metalanguage and an operational cost semantics plus two denotational semantics: a distribution-over-(cost,output) cost semantics and an… | ||
| A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and(…) | Cunyuan Gao, Lionel Parreaux | 14m |
A new system named InvalML statically tracks both permanent and temporary invalidation for regioned resources by combining Boolean-algebraic types (unions… | ||
| Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing(…) | Zachary Grannan, Aurel Bílý, Jonáš Fiala, Jasper Geer, Markus de Medeiros, Peter Müller, Alexander J. Summers | 16m |
Place Capability Graphs (PCG) present a concretely computable model of Rust ownership that is extracted from the compiler’s MIR and borrow-checker facts and… | ||
| LOUD: Synthesizing Strongest and Weakest Specifications | Kanghee Park, Xuanyu Peng, Loris D'Antoni | 14m |
The paper presents LOUD, a logic and algorithm that synthesizes strongest L-consequences (over-approximations) and weakest L-implicants (under-approximations)… | ||
| Reasoning about External Calls | Julian Mackay, Sophia Drossopoulou, James Noble, Susan Eisenbach | 17m |
Paper proposes concrete assertions and a verification calculus that prove internal code cannot lose funds despite invoking unknown external objects. It models… | ||
| SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races | Reese Levine, Ashley Lee, Neha Abbas, Kyle Little, Tyler Sorensen | 15m |
Identifies a WGSL specification gap where data races let downstream GPU compilers legally remove bounds clamps, enabling out‑of‑bounds accesses; implements a… | ||
| Structural Abstraction and Refinement for Probabilistic Programs | Guanyan Li, Juanen Li, Zhilei Han, Peixin Wang, Hongfei Fu, Fei He | 15m |
Framework treats a Probabilistic Control‑Flow Automaton as an MDP whose actions drop semantics, so the structural upper bound is the MDP’s maximum reachability… | ||
| Pyrosome: Verified Compilation for Modular Metatheory | Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala | 16m |
Pyrosome is a Coq framework that defines languages as lists of inference rules (GATs) and treats program equivalence as the reflexive‑transitive‑symmetric… | ||
| DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance | Chenyang Ma, Wei Song, Jeff Huang | 12m |
DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance (Video, OOPSLA2 2025)
Chenyang Ma, Wei Song, and Jeff Huang
(Nanjing University of… | ||
| IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis | Aman Nougrahiya, V Krishna Nandivada | 16m |
Algorithm IncIDFA produces precise incremental variants for any monotone IDFA using a two-pass approach plus per-SEC stabilization and safe/under-approximated… | ||
| Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and(…) | Radosław Jan Rowicki, Adrian Francalanza, Alceste Scalas | 13m |
Claims a distributed black-box monitoring algorithm that is sound and complete for detecting deadlocked services in RPC/gen_server-style systems, proved and… | ||
| Cost of Soundness in Mixed-Precision Tuning | Anastasia Isychev, Debasmita Lohar | 15m |
Compares five open-source mixed-precision tuners on 100 FPBench straight-line programs and measures speedup, error budget usage, and runtime. Key findings… | ||
| The Simple Essence of Monomorphization | Matthew Lutze, Philipp Schuster, Jonathan Immanuel Brachthäuser | 14m |
Presents a type-flow directed monomorphization that duplicates declarations by collecting type-flow constraints, solving them with a fixed-point graph… | ||
| im2im: Automatically Converting In-Memory Image Representations using A Knowledge(…) | Fei Chen, Sunita Saha, Manuela Schuler, Philipp Slusallek, Tim Dahmen | 14m |
im2im is a Python library that builds a knowledge graph of 1:1 metadata nodes for in‑memory image representations (NumPy/OpenCV, Pillow, PyTorch, scikit‑image… | ||
| A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning(…) | Kartik Chandra, Tony Chen, Joshua B. Tenenbaum, Jonathan Ragan-Kelley | 16m |
Memo is a domain-specific probabilistic programming language for recursive theory-of-mind models that compiles to JAX and runs on GPUs. It embeds in Python… | ||
| Translation Validation for LLVM's AArch64 Backend | Ryan Berger, Mitch Briles, Nader Boushehrinejad Moradi, Nicholas Coughlin, Kait Lam, Nuno P. Lopes, Stefan Mada, Tanmay Tirpankar, John Regehr | 15m |
arm-tv is a translation validator that lifts AArch64 assembly to LLVM MIR, extends Alive2 to handle mixed pointer/integer code and adds a flat memory model and… | ||
| We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators | Patrick LaFontaine, Zhe Zhou, Ashish Mishra, Suresh Jagannathan, Benjamin Delaware | 16m |
A tool called Cobb repairs incomplete OCaml input generators by synthesizing code that fills typed holes so the generator’s range includes every valid input… | ||
| ROSpec: A Domain-Specific Language for ROS-based Robot Software | Paulo Canelas, Bradley Schmerl, Alcides Fonseca, Christopher Steven Timperley | 14m |
A DSL that encodes ROS component constraints and checks integration before run time, using liquid and dependent types over parameters, topics and QoS… | ||
| Bridging the Gap between Real-World and Formal Binary Lifting through(…) | Jihee Park, Insu Yun, Sukyoung Ryu | 14m |
Defines correctness as filtered-simulation and formalizes three concrete transformations: control flow graph reconstruction, abstract stack reconstruction, and… | ||
| Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing | Qiong Feng, Xiaotian Ma, Ziyuan Feng, Marat Akhin, Wei Song, Peng Liang | 14m |
Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing (Video, OOPSLA2 2025)
Qiong Feng, Xiaotian Ma, Ziyuan Feng, Marat Akhin… | ||
| QbC: Quantum Correctness by Construction | Anurudh Peduri, Ina Schaefer, Michael Walter | 13m |
Presents a method that builds quantum programs from pre/postconditions by applying sound and complete refinement rules over a quantum while language, using… | ||
| JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from(…) | Hanzhang Wang, Wei Peng, Wenwen Wang, Yunping Lu, Pen-Chung Yew, Weihua Zhang | 15m |
Prototype JIT for Android 14 uses translation rules learned offline from existing JITs, extracts ~5k rules in ~10 minutes, verifies them with symbolic… | ||
| Destination calculus: A linear λ-calculus for purely functional memory writes | Thomas BAGREL, Arnaud Spiwack | 14m |
Presents a concrete calculus that compiles destination‑passing into pure functional code and shows nontrivial examples: a tail‑recursive map implemented with… | ||
| (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging | Yaozhu Sun, Xuejing Huang | 15m |
A compiler for the CP language compiles dynamic inheritance via a merge operator into runtime extensible records with mangled type labels, proving type safety… | ||
| Soundness of Predictive Concurrency Analyses | Shuyang Liu, Doug Lea, Jens Palsberg | 15m |
Presents a unified, graph‑based definition of soundness for predictive concurrency analyses, lifts trace state‑similarity to execution‑graph similarity with… | ||
| ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications | Jiarun Dai, Mingyuan Luo, Yuan Zhang, Min Yang, Minghui Yang | 13m |
Builds and open-sources ApkDiffer, a method-level Android diffing tool that splits each app into two-stage decomposition of event-driven functionality units… | ||
| Detecting and explaining (in-)equivalence of context-free grammars | Marko Schmellenkamp, Thomas Zeume, Sven Argo, Sandra Kiefer, Cedric Siems, Fynn Stebel | 15m |
A scalable framework decides, proves, and explains many (in-)equivalences of context-free grammars despite undecidability by combining a new pattern-based… | ||
| Qualified Types with Boolean Algebras | Edward Lee, Jonathan Lindegaard Starup, Ondřej Lhoták, Magnus Madsen | 15m |
Proposes qualifier-backed effects using Boolean algebras by formalizing System F⧼:B (negation, qualifier polymorphism, subqualification) and deriving an effect… | ||
| Non-interference Preserving Optimising Compilation | Julian Rosemann, Sebastian Hack, Deepak Garg | 14m |
Introduces hyperproperty simulations as a new secure-compilation framework that models preservation of arbitrary k‑hyperproperties and proves a generic… | ||
| Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with(…) | Ruixin Wang, Zhongkai Zhao, Le Fang, Nan Jiang, Yiling Lou, Lin Tan, Tianyi Zhang | 14m |
iFix instruments code using call-graph and def‑use analysis, runs failing tests on multiple patched copies, aligns per-variable runtime values into a runtime… | ||
| Checking Observational Correctness of Database Systems | Lauren Pick, Amanda Xu, Ankush Desai, Sanjit A. Seshia, Aws Albarghouthi | 14m |
Tool encodes transaction behavior with a version-aware semantics and checks isolation via explicit SMT constraints so the checker asks whether any valid… | ||
| A complete formal semantics of eBPF instruction set architecture for Solana | Shenghao Yuan, Zhuoruo Zhang, Jiayi Lu, David Sanan, Rui Chang, Yongwang Zhao | 13m |
First complete formal semantics for Solana eBPF, mechanized as a small‑step operational model that covers 116 opcodes and is extracted to executable… | ||
| HeapBuffers: Why not just using a binary serialization format for your managed memory? | Daniele Bonetta, Júnior Löff, Matteo Basso, Walter Binder | 16m |
HeapBuffers stores Java objects off-heap FlatBuffers layout in a separate transferable heap, generates schema-specific GC and specialized Java code, and… | ||
| Borrowing From Session Types | Hannes Saffrich, Janek Spaderna, Peter Thiemann | 15m |
Proposes BGV, a session‑type API that replaces resource‑passing with borrowing via a split primitive that carves a channel into a single‑action borrow and a… | ||
| Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation | Philipp Schuster, Marius Müller, Klaus Ostermann, Jonathan Immanuel Brachthäuser | 13m |
An intermediate representation called Xcut intermediate representation encodes classical sequent calculus as a normalized term language with formal typing and… | ||
| A Refinement Methodology for Distributed Programs in Rust | Aurel Bílý, João Pereira, Peter Müller | 14m |
Presents a bottom-up refinement method that pairs guarded transition systems with a novel locally inductive invariants proof rule, implemented as a Rust… | ||
| Laurel: Unblocking Automated Verification with Large Language Models | Eric Mugnier, Emmanuel Anaya Gonzalez, Nadia Polikarpova, Ranjit Jhala, Zhou Yuanyuan | 15m |
Laurel is a tool that generates missing Dafny assertions with LLMs by (1) inserting an assertion placeholder at the SMT error location and (2) supplying… | ||
| QED in Context: An Observation Study of Proof Assistant Users | Jessica Shi, Cassia Torczon, Harrison Goldstein, Benjamin C. Pierce, Andrew Head | 19m |
An observational study watches 30 proof assistant users (half Rocq and Lean) for ~1 hour each and surfaces four concrete findings: proofs evolve nonlinearly… | ||
| Flexible and Expressive Typed Path Patterns for GQL | Wenjia Ye, Matías Toro, Tomas Diaz, Manuel Rigger, Claudio Gutierrez, Domagoj Vrgoč | 16m |
Defines FPPC — a formal type calculus for a core GQL fragment that adds property filters and imprecise (unknown) types, and statically flags queries that are… | ||
| Finch: Sparse and Structured Tensor Programming with Control Flow | Willow Ahrens, Teodoro F. Collin, Radha Patel, Kyle Deeds, Changwan Hong, Saman Amarasinghe | 15m |
Finch is a new language and compiler that combines flexible control flow with a parameterized format DSL to generate code that iterates only over nonzeros and… | ||
| Static Inference of Regular Grammars for Ad Hoc Parsers | Michael Schröder, Jürgen Cito | 16m |
Automatic system PANINI uses a lambda-Σ IR, refinement-type inference and a novel abstract-interpretation quantifier-elimination to turn string verification… | ||
| Understanding and Improving Flaky Test Classification | Shanto Rahman, Saikat Dutta, August Shi | 15m |
Shows that prior flaky-test classifiers leak data and use unrealistic mixes so reported F1 falls from 81.82% to 56.62% after fixes; builds a realistic dataset… | ||
| Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification | Chenghang Shi, Dongjie He, Haofeng Li, Jie Lu, Lian Li, Jingling Xue | 14m |
MoYe is a regularization-based graph simplification that prunes edges that cannot lie on any CFL-reachable source-to-sink path by over-approximating the… | ||
| Two Approaches to Fast Bytecode Frontend for Static Analysis | Chenxi Li, Haoran Lin, Tian Tan, Yue Li | 15m |
A new Java bytecode frontend implemented in Tai-e translates stack bytecode into SSA-capable 3-address IR using pattern-aware 3-address code translation to… | ||
| Adequacy for Algebraic Effects Revisited | Alex Kavvos | 14m |
Proves an adequacy theorem that covers a wide class of algebraic effects including infinitary cases, showing that denotational equality in a Call-by-Push-Value… | ||
| Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through(…) | Humphrey Burchell, Stefan Marr | 15m |
Paper approximates profiler ground truth by injecting CPU‑wasting movs at machine‑code basic‑block boundaries and using hardware counters to tune the slowdown… | ||
| Convex Hull Approximation for Activation Functions | Zhongkui Ma, Zihan Wang, Guangdong Bai | 14m |
WraAct constructs tight polyhedral over-approximations of activation convex hulls by introducing linear constraints that smooth activations into… | ||
| Quantified Underapproximation via Labeled Bunches | Lang Liu, Farzaneh Derakhshan, Limin Jia, Gabriel A. Moreno, Mark Klein | 14m |
Presents a formal system that lets over‑ and under‑approximate analyses compose soundly by attaching a test-level modality that ranges over component internal… | ||
| Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic | Shushu Wu, Xiwei Wu, Qinxiang Cao | 13m |
Claims a mechanical reduction of ∀∃ relational Hoare triples to ordinary unary Hoare triples by redefining relational validity and internalizing the ∀∃ pattern… | ||
| Incremental Certified Programming | Tomas Diaz, Kenji Maillard, Nicolas Tabareau, Éric Tanter | 15m |
Claims a formal framework that makes specifications monotone over partial programs by defining a completion refinement relation and a notion of completeness… | ||
| UTFix: Change Aware Unit Test Repairing using LLM | Shanto Rahman, Sachit Kuhar, Berk Cirisci, Pranav Garg, Shiqi Wang, Xiaofei Ma, Anoop Deoras, Baishakhi Ray | 14m |
UTFix uses LLM prompts plus static and dynamic code slicing to repair test assertions and restore coverage, taking original and updated focal methods, the… | ||
| Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection | Dowon Song, Hakjoo Oh | 14m |
PRISM builds a custom static analyzer that extracts 11 semantic properties (defs/uses, memory values, exceptions) and represents patches as a semantic feature… | ||
| Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…) | Maolin Sun, Yibiao Yang, Jiangchang Wu, Yuming Zhou | 15m |
Aries validates SMT rewriters by combining mimetic mutation that reshapes seed formulas to match rewrite left‑hand sides with generative equality saturation… | ||
| Work Packets: A New Abstraction for GC Software Engineering, Optimization, and(…) | Wenyu Zhao, Stephen M. Blackburn, Kathryn S McKinley | 17m |
Proposes a work packet abstraction implemented in MMTk that breaks GC into tiny work items, small hot kernels, and schedulable packets, replacing coarse phase… | ||
| Scaling Instruction-Selection Verification against Authoritative ISA Semantics | Michael McLoughlin, Ashley Sheng, Chris Fallin, Bryan Parno, Fraser Brown, Alexa VanHattum | 14m |
Arrival verifies Cranelift instruction selection end to end by composing rules (rule chaining) and auto‑deriving ISA specs from vendor ASL via a… | ||
| Automated Discovery of Tactic Libraries for Interactive Theorem Proving | Yutong Xin, Jimmy Xin, Gabriel Poesia, Noah D. Goodman, Qiaochu Chen, Işıl Dillig | 11m |
A tool called TacMineR builds Tactic Dependence Graphs (TDGs) that encode formal input/output dependencies between tactic applications, finds isomorphic… | ||
| Fast Constraint Synthesis for C++ Function Templates | Shuo Ding, Qirun Zhang | 13m |
A Clang frontend implements a lightweight interprocedural static analysis that encodes uses in a function body as constraints, composes them with conjunctions… | ||
| Modal Effect Types | Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, Anton Lorenzen | 14m |
Replaces pervasive effect variables with an ambient effect context and explicit modalities so higher‑order library signatures no longer need ubiquitous effect… | ||
| Opportunistically Parallel Lambda Calculus | Stephen Mell, Konstantinos Kallas, Steve Zdancewic, Osbert Bastani | 14m |
Proposes an evaluation strategy and core calculus (Opportunistic Lambda Calculus) that dispatches independent external calls as holes, resolves them… | ||
| Tracing Just-in-time Compilation for Effects and Handlers | Marcial Gaißert, CF Bolz-Tereick, Jonathan Immanuel Brachthäuser | 15m |
Implements an RPython-based tracing JIT that runs a common bytecode target for Eff, Effekt, and Koka, records hot traces and applies allocation removal and… | ||
| Combining Formal and Informal Information in Bayesian Program Analysis via Soft(…) | Tianchi Li, Xin Zhang | 16m |
Converts a Datalog analysis into a Bayesian network, attaches rule probabilities, and injects neural-network confidences as soft evidence (implemented via a… | ||
| A Sound Static Analysis Approach to I/O API Migration | Shangyu Li, Zhaoyang Zhang, Sizhe Zhong, Diyu Zhou, Jiasi Shen | 14m |
Sprout automatically migrates C programs between I/O APIs and guarantees behavioral equivalence by synthesizing replacement code from API specs and program… | ||
| A Hoare Logic For Symmetry Properties | Vaibhav Mehta, Justin Hsu | 14m |
Defines a Hoare-style program logic where pre/post assertions are composable group actions (syntax for group operations and entailment), implements a prototype… | ||
| HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines | Vladyslav Nekriach, Sidi Mohamed Beillahi, Chenxing Li, Peilun Li, Ming Wu, Andreas Veneris, Fan Long | 15m |
HEMVM integrates EVM and MoveVM inside an Aptos-based prototype by adding two system APIs and an invoker/handler pattern so contracts call across VMs… | ||
| Debugging WebAssembly? Put some Whamm on it! | Elizabeth Gilbert, Matthew Schneider, Zixi An, Suhas Thalanki, Wavid Bowman, Alexander Bai, Ben L. Titzer, Heather Miller | 16m |
Whamm is an instrumentation framework for WebAssembly that compiles a declarative DSL into either an engine-level Whey engine API probe module or a… | ||
| KestRel: Relational Verification Using E-Graphs for Program Alignment | Robert F. Dickerson, Prasita Mukherjee, Benjamin Delaware | 15m |
KestRel builds an intermediate product program via an algebra of alignments, represents the rewrite search in e-graphs and equality saturation, and extracts… | ||
| Software Model Checking via Summary-Guided Search | Ruijie Fang, Zachary Kincaid, Thomas Reps | 16m |
GPS presents a concrete algorithm that interleaves directed testing with summary-guided search: it queries an SMT solver for models, uses a summary oracle… | ||
| Advancing Performance via a Systematic Application of Research and Industrial Best(…) | Wenyu Zhao, Stephen M. Blackburn, Kathryn S McKinley, Man Cao, Sara S. Hamouda | 17m |
Productized LXR into Google’s environment, implemented in MTK with OpenJDK11, and closes the gap with specialized production collectors: optimized LXR… | ||
| SafeTree: Expressive Tree Policies for Microservices | Karuna Grewal, Brighten Godfrey, Justin Hsu | 15m |
Defines a policy language that compiles to a visibly pushdown automata and proves the compilation is sound for nested-word views of service-call trees… | ||
| Polynomial Bounds of CFLOBDDs against BDDs | Xusheng Zhi, Thomas Reps | 15m |
Shows that, given the same variable ordering, a CFLOBDD for any Boolean function is at most polynomially larger than a BDD: groupings count = O(b log b)… | ||
| Quantization with Guaranteed Floating-Point Neural Network Classifications | Anan Kabaha, Dana Drachsler Cohen | 15m |
CoMPAQt computes a maximal classification-confidence bound using a novel MILP encoding of quantization plus customized linear relaxations and constraints that… | ||
| Interleaving Large Language Models for Compiler Testing | Yunbo Ni, Shaohua Li | 15m |
A two‑phase framework decouples expensive LLM use: an offline database of 500,000 validated functions generated and profiled by LLMs, and an online composition… | ||
| Automatically Verifying Replication-aware Linearizability | Vimala Soundarapandian, Kartik Nagar, Aseem Rastogi, KC Sivaramakrishnan | 14m |
Automated verification framework proves replication-aware linearizability for Mergeable Replicated Data Types by checking novel algebraic laws on the three-way… | ||
| Mini-Batch Robustness Verification of Deep Neural Networks | Saar Tzour-Shaday, Dana Drachsler Cohen | 17m |
BaVerLy is a sound and complete verifier that jointly verifies mini-batches of ε-balls by encoding networks as MILP and grouping inputs with activation-pattern… | ||
| Zero-Overhead Lexical Effect Handlers | Cong Ma, Zhaoyi Ge, Jonghyun Jung, Yizhou Zhang | 15m |
Claims a zero-overhead implementation for lexically scoped exceptional effect handlers via a type-directed translation that emits static provenance metadata… | ||
| What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data(…) | Yichen Xu, Oliver Bračevac, Nguyen Pham, Martin Odersky | 16m |
Claims a new calculus System Capless with existential and universal capture-set quantification and a named mechanism rcaps that lets generic boxed capabilities… | ||
| Synthesizing Implication Lemmas for Interactive Theorem Proving | Ana Brendel, Aishwarya Sivaraman, Todd Millstein | 14m |
Implements a Rocq tactic called dilemma that synthesizes implication lemmas of the form P1 ∧ … ∧ Pn ⇒ Q by data-driven invariant inference over sample… | ||
| Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge | John C. Kolesar, Shan Ali, Timos Antonopoulos, Ruzica Piskac | 14m |
Crepe is a zero-knowledge protocol that encodes full regular-expression equivalence proofs (PSPACE-complete) using a custom calculus based on coinduction and… | ||
| Revealing Sources of (Memory) Errors via Backward Analysis | Flavio Ascari, Roberto Bruni, Roberta Gori, Francesco Logozzo | 13m |
Claims a new backward under‑approximation proof system called SIL and a memory‑aware specialization Separation SIL that are sound and (relatively) complete for… | ||
| Divide and Conquer: A Compositional Approach to Game-Theoretic Security | Ivana Bocevska, Anja Petković Komel, Laura Kovács, Sophie Rain, Michael Rawson | 14m |
Compositional pipeline reduces game-theoretic blockchain security checks to many small SMT queries instead of one huge one, encoding incentives in first-order… | ||
| Code Style Sheets: CSS for Code | Sam Cohen, Ravi Chugh | 14m |
A system that generalizes CSS selectors to ASTs for algebraic data types and a bidirectional view model lets styles target source-level patterns and propagate… | ||
| Carapace: Static–Dynamic Information Flow Control in Rust | Vincent Beardsley, Chris Xiong, Ada Lamba, Michael D. Bond | 15m |
Carapace implements hybrid static–dynamic information flow control for unmodified Rust via a library and macros that add secure blocks and generated runtime… | ||
| Float Self-Tagging | Olivier Melançon, Manuel Serrano, Marc Feeley | 14m |
Introduces an invertible bitwise transform called self-tagging that maps a subset of IEEE754 doubles into tagged machine words so value and type share one… | ||
| Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers | Arya Vohra, Leo Seojun Lee, Jakub Bachurski, Oleksandr Zinenko, Phitchaya Mangpo Phothilimthana, Albert Cohen, William S. Moses | 13m |
Equality saturation is integrated into XLA with a C++/Rust egraph pass that replaces brittle local rewrites with a global cost model, yielding an average 3.45%… | ||
| Agora: Trust Less and Open More in Verification for Confidential Computing | Hongbo Chen, Quan Zhou, Sen Yang, Sixuan Dang, Xing Han, Danfeng Zhang, Fan Zhang, XiaoFeng Wang | 16m |
Agora implements a prototype verification platform that pushes heavy static analysis and SMT solving out of the TCB, replacing them with a tiny in-enclave… | ||
| Polymorphic Records for Dynamic Languages | Giuseppe Castagna, Loïc Peyrot | 15m |
Extends semantic subtyping to support row polymorphism alongside union, intersection and negation types, defines a λ-calculus with record extension, selection… | ||
| Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM | Ao Li, Byeongjee Kang, Vasudev Vikram, Isabella Laybourn, Samvid Dharanikota, Shrey Tiwari, Rohan Padhye | 16m |
Fray is a JVM concurrency testing platform that orchestrates thread interleavings without replacing primitives using shadow locking, enabling deterministic… | ||
| Sound and Modular Activity Analysis for Automatic Differentiation in MLIR | Mai Jacob Peng, William S. Moses, Oleksandr Zinenko, Christophe Dubach | 14m |
Implements a sound abstract interpretation of activity analysis inside MLIR, formalizing an MLIR subset amenable to AD and proving correctness; adds a modular… | ||
| React-tRace: A Semantics for Understanding React Hooks | Jay Lee, Joongwon Ahn, Kwangkeun Yi | 14m |
A formal operational semantics called React-tRace models core Hook behavior (useState and useEffect) and ships a stepwise visualizer online that replays… | ||
| Pathological Cases for a Class of Reachability-Based Garbage Collectors | Matthew Sotoudeh | 14m |
Paper proves that any reachability-based GC that implements a realistic mutator‑observer interface has a pathological program forcing it to either long GC… | ||
| Syntactic Completions with Material Obligations | David Moon, Andrew Blinn, Thomas J. Porter, Cyrus Omar | 15m |
Prototype editor tall tylr completes malformed code by inserting abstract syntactic placeholders rather than enumerating text repairs, using a tile-based… | ||
| Embedding Quantum Program Verification into Dafny | Feifei Cheng, Sushen Vangeepuram, Henry Allard, Seyed Mohammad Reza Jafari, Alex Potanin, Liyi Li | 14m |
QafnyC compiles quantum program verification into Dafny and then down to executable circuits (via Sqir/OpenQASM), implementing a type-driven verifier that… | ||
| Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations | Guofeng Cui, Yuning Wang, Wensen Mao, Yuanlin Duan, He Zhu | 15m |
RoboScribe automatically derives state predicates and abstract actions from raw unsegmented demonstrations, alternates comparative abstraction refinement with… | ||
| AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators | Avner Bensoussan, Elena Chachkarova, Karine Even-Mendoza, Sophie Fortz, Connor Lenihan | 15m |
A framework automatically tunes variational quantum eigensolver implementations by treating them as black-box programs, training an XGBoost regressor on… | ||
| Semantics of Sets of Programs | Jinwoo Kim, Shaan Nagy, Thomas Reps, Loris D'Antoni | 15m |
Claims that compositional verification of simple properties for infinite program sets with loops requires tracking behaviors across unbounded executions, and… | ||
| Towards Verifying Crash Consistency | Keonho Lee, Conan Truong, Brian Demsky | 15m |
Guarantees crash consistency for well-typed implementations by proving a type system and compiling to Rust that inserts fences/flushes; the paper ships a… | ||
| Metamorph: Synthesizing Large Objects from Dafny Specifications | Aleksandr Fedchin, Alexander Bai, Jeffrey S. Foster | 13m |
Metamorph synthesizes long sequences of Dafny-specified API calls by replaying verifier counterexamples one step at a time and framing search as weighted A… | ||
| Certified Decision Procedures for Width-Independent Bitvector Predicates | Siddharth Bhat, Leo Stefanesco, Chris Hughes, Tobias Grosser | 16m |
Mechanized, executable decision procedures in Lean for width-independent bitvectors that formalize k-induction, automata reachability, emptiness checking and… | ||
| An Empirical Evaluation of Property-Based Testing in Python | Savitha Ravi, Michael Coblenz | 14m |
Corpus study of 426 Python projects using Hypothesis classifies PBTs into 12 dataflow-based categories, runs mutation testing on 40 projects, and reports an… | ||
| RestPi: Path-Sensitive Type Inference for REST APIs | Mark W. Aldrich, Kyla H. Levin, Michael Coblenz, Jeffrey S. Foster | 15m |
REST𝜋 implements path-sensitive type inference for Ruby on Rails servers and automatically generates OpenAPI‑style specs by encoding symbolic path constraints… | ||
| Adaptive Shielding via Parametric Safety Proofs | Yao Feng, Jun Zhu, André Platzer, Jonathan Laurent | 14m |
A programming-language framework implements parametric safety proofs that let a shield start conservative and become permissive as runtime knowledge is… | ||
| Inductive Synthesis of Inductive Heap Predicates | Ziyi Yang, Ilya Sergey | 13m |
Claim: an algorithm synthesises recursive Separation Logic predicates from concrete heap graphs using positive-only ILP encoded in answer set programming… | ||
| Unveiling Heisenbugs with Diversified Execution | Arjun Ramesh, Tianshu Huang, Jaspreet Riar, Ben L. Titzer, Anthony Rowe | 14m |
Presents a concrete system and results: a WebAssembly-backed dynamic data-race detector called Beanstalk that uses trap delay injection and stochastic partial… | ||
| nothing matches | ||