PLDI 2025
2025-06-16..2025-06-20
Seoul, South Korea
[PLDI 2020, PLDI 2022, PLDI 2023, PLDI 2024, PLDI 2024 Workshop Honoring Andreas Podelski, PLDI 2025, PLDI 2026, PLDI 2026 Student Research Competition]
| title | author | length |
|---|---|---|
| Programming Language Research for Technical and Social Good: What PL Can Do for Good? | Sukyoung Ryu | 01h 02m |
Group builds executable, mechanized language specifications and uses them to auto-generate parsers, interpreters, and test suites; JavaScript DSL ESmeta… | ||
| Lean: Machine-Checked Mathematics and Verified Programming, Past and Future | Leonardo de Moura | 01h 08m |
Lean claims a small trusted core and full extensibility, with 2 million lines in Mathlib and 100,000 theorems verified; automation like grinds and a verified… | ||
| Neurosymbolic Program Synthesis: Bridging Perception and Reasoning in Real-World(…) | Işıl Dillig | 01h 10m |
Neurosymbolic Program Synthesis combines pretrained neural primitives (vision models, classifiers, LLMs) with DSLs and symbolic constructs, using LLM-guided… | ||
| Nola: Later-Free Ghost State for Verifying Termination in Iris | Yusuke Matsushita, Takeshi Tsukada | 20m |
Nola presents a concrete method to remove Iris’s obstructive later modality by encoding shared state as syntactic SL formulas and giving them a separate… | ||
| Sound Static Data Race Verification for C: Is the Race Lost? | Karoliine Holter, Simmo Saan, Patrick Lam, Vesal Vojdani | 18m |
Paper evaluates SV-COMP race verifiers on real C programs and on extracted micro-benchmarks that codify common multithreaded idioms, measuring soundness and… | ||
| Efficient Linearizability Monitoring | Parosh Aziz Abdulla, Samuel Grahn, Bengt Jonsson, Krishna Shankaranarayanan, Om Swostik Mishra | 19m |
Revisits monitoring linearizability for stacks queues and (multi)sets and gives concrete algorithms with proven complexities: stacks O(n^2), queues O(n log n)… | ||
| Efficient Timestamping for Sampling-Based Race Detection | Minjian Zhang, Daniel Wee Soong Lim, Mosaad Al Thokair, Umang Mathur, Mahesh Viswanathan | 19m |
Proposes a sampling-aware timestamp scheme that replaces full vector-clock updates with a freshness timestamp and an ordered vector clock data structure… | ||
| RRR-SMR: Reduce, Reuse, Recycle: Better Methods for Practical Lock-Free Data Structures | Md Amit Hasan Arovi, Ruslan Nikolaev | 20m |
Method that lets nodes move between lock free structures without reallocation by combining compare-and-swap tags for ABA safety, a strict ownership model with… | ||
| CRGC: Fault-Recovering Actor Garbage Collection in Pekko | Dan Plyukhin, Gul Agha, Fabrizio Montesi | 25m |
CRGC implements the first fault-recovering cyclic actor GC for distributed actor systems and ships a Java prototype in Apache Pekko. It records local actor… | ||
| Iso: Request-Private Garbage Collection | Tianle Qiu, Stephen M. Blackburn | 16m |
Claim: a practical request-private GC for Java that uses opportunistic copying on an Immix-style mark-region heap to avoid global pauses. Implemented in… | ||
| Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals | Janggun Lee, Jeonghyeon Kim, Jeehoon Kang | 14m |
Presents a new hazard-pointer validation that exploits the immutability of marked nodes to validate reachability by checking the most recent unmarked… | ||
| Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic | Jaehwang Jung, Sunho Park, Janggun Lee, Jeho Yeon, Jeehoon Kang | 19m |
First formal verification of a general-purpose RCU under relaxed memory consistency, proving a modular spec that supports modular specification, switchable… | ||
| Efficient, Portable, Census-Polymorphic Choreographic Programming | Mako P. Bates, Shun Kashiwa, Syed Usman Jafri, Gan Shen, Lindsey Kuper, Joseph P. Near | 20m |
Claims that conclaves and multiply-located values remove redundant broadcasts and make conditionals communication-efficient, with a formal lambda-C showing… | ||
| Principal Type Inference under a Prefix: A Fresh Look at Static Overloading | Daan Leijen, Wenjia Ye | 20m |
A new rule set, HMQ (type inference under a prefix), replaces HM guessing with fresh type variables plus composable prefixes as solvable constraints, yielding… | ||
| Tree Borrows | Neven Villani, Johannes Hostert, Derek Dreyer, Ralf Jung | 20m |
Replaces Stacked Borrows’ stack with a per-allocation tree and formalizes aliasing rules so compilers can assume those violations are UB while accepting many… | ||
| Efficient Formal Verification of Quantum Error Correcting Programs | Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying | 22m |
An assertion-and-program logic with a sound proof system converts Pauli-error verification conditions into purely classical formulas solved by SMT solvers, and… | ||
| QVM: Quantum Gate Virtualization Machine | Nathaniel Tornow, Emmanouil Giortamis, Pramod Bhatotia | 17m |
QVM exposes a virtual circuit IR plus a compiler and runtime that split circuits into optimized fragments, schedule them across small QPUs, and classically… | ||
| Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs | Zhicheng Zhang, Mingsheng Ying | 20m |
Proposes a new quantum register machine architecture plus an instruction set (QINS) and a compilation pipeline that compiles RQ++ recursive programs into… | ||
| MarQSim: Reconciling Determinism and Randomness in Compiler Optimization for Quantum(…) | Xiuqi Cao, Junyu Zhou, Yuhao Liu, Yunong Shi, Gushu Li | 20m |
MarQSim builds a Markov-chain HTT graph of Hamiltonian terms, turns transition-matrix design into a constrained minimum-cost flow problem that encodes… | ||
| Optimizing Ancilla-Based Quantum Circuits with SPARE | Ritvik Sharma, Sara Achour | 19m |
SPARE is a rewrite-based optimizer that detects and restructures compute–uncompute (CTU) patterns in QPL-lowered circuits and uses ancilla state propagation to… | ||
| Guided Tensor Lifting | Yixuan Li, Alexander Brauckmann, Michael F. P. O'Boyle, Elizabeth Polgreen | 19m |
Automatic lifting from C to Taco uses an LLM to generate 10 candidate tensor expressions, extracts a probabilistic grammar from those samples, and drives… | ||
| Scalable, Validated Code Translation of Entire Projects using Large Language Models | Hanliang Zhang, Cristina David, Meng Wang, Brandon Paulsen, Daniel Kroening | 20m |
An LLM-based pipeline translates whole Go repositories to Rust by partitioning code into functions/types, prompting with predefined feature mapping rules (e.g… | ||
| Reductive Analysis with Compiler-Guided Large Language Models for Input-Centric Code(…) | Xiangwei Wang, Xinning Hui, Chunhua Liao, Xipeng Shen | 18m |
Uses a compiler-guided LLM pipeline that applies reductive analysis over the call graph, one function at a time, with prompt templates and a map-reduce token… | ||
| Type-Constrained Code Generation with Language Models | Niels Mündler, Jingxuan He, Hao Wang, Koushik Sen, Dawn Song, Martin Vechev | 21m |
Introduces a type-constrained decoding method that integrates an incremental type checker into token-level LLM decoding using prefix automata plus a search… | ||
| Bean: A Language for Backward Error Analysis | Ariel E. Kellison, Laura Zielinski, David Bindel, Justin Hsu | 24m |
Bean is a typed first-order language that encodes backward error via a graded coeffect system with strict linearity and a categorical semantics proving… | ||
| Correctly Rounded Math Libraries without Worrying about the Application’s Rounding Mode | Sehyeok Park, Kim Justin, Santosh Nagarakatte | 22m |
RLibm generates correctly rounded elementary functions and this work builds two ways to avoid costly rounding-mode switches: round-to-zero emulation replaces… | ||
| Support Triangle Machine | Jiaying Li, Chunxue Hao | 20m |
Presents a constructive algorithm that lifts single-neuron convex approximations into multi-neuron ones by iteratively decomposing each output coordinate into… | ||
| Solving Floating-Point Constraints with Continuous Optimization | Qian Chen, Chenqi Cui, Fengjuan Gao, Yu Wang, Ke Wang, Linzhang Wang | 19m |
Grater converts floating‑point formulas into continuous, piecewise‑linear objective functions and uses gradient descent with random starts to find global… | ||
| Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic(…) | Cameron Moy, Jack Czenszak, John M. Li, Brianna Marshall, Steven Holtzen | 22m |
Roulette claims to be the first discrete PPL that pairs exact, scalable inference with a large subset of Racket features (data structures, first‑class… | ||
| Stochastic Lazy Knowledge Compilation for Inference in Discrete Probabilistic Programs | Maddy Bowers, Alexander K. Lew, Joshua B. Tenenbaum, Armando Solar-Lezama, Vikash K. Mansinghka | 22m |
Implements lazy knowledge compilation in a Julia tool called Pluck and combines it with sequential Monte Carlo that uses locally‑optimal proposals computed… | ||
| Probabilistic Refinement Session Types | Qiancheng Fu, Ankush Das, Marco Gaboardi | 22m |
Introduces PReST, a core calculus that generalizes probabilistic session types to symbolic probabilities and proves type safety, global progress, probability… | ||
| Semantics of Integrating and Differentiating Singularities | Jesse Michel, Wonyeol Lee, Hongseok Yang | 19m |
A formal semantics for programs that evaluate and differentiate singular integrals, giving a denotational model and an operational Monte Carlo estimator that… | ||
| Random Variate Generation with Formal Guarantees | Feras A. Saad, Wonyeol Lee | 22m |
Automated synthesis produces exact random variate generators from a finite-precision CDF and a C library implements them using fast integer arithmetic (no… | ||
| Relational Abstractions Based on Labeled Union-Find | Dorian Lesbre, Matthieu Lemerre, Hichem Ait-El-Hara, François Bobot | 21m |
Introduces a data structure that extends union‑find by storing group‑valued labels on parent edges to represent injective relations such as y = ax + b… | ||
| Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses | Fabian Stemmler, Michael Schwarz, Julian Erhard, Sarah Tilscher, Helmut Seidl | 20m |
Proposes three concrete fixes — narrowing per origin, reluctant widening, and abstract garbage collection — that decouple global updates via an update rules… | ||
| LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols | Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, Zhong Shao | 19m |
LiDO-DAG gives an abstract concurrent-object model and a refinement proof showing DAG protocols simulate leader-based consensus, implemented in Coq and… | ||
| PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs | Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy | 20m |
PulseCore is a new, mechanized concurrent separation logic implemented inside F★ that claims to support impredicative invariants and higher‑order ghost state… | ||
| Thrust: A Prophecy-Based Refinement Type System for Rust | Hiromi Ogawa, Taro Sekiyama, Hiroshi Unno | 20m |
A new Rust verifier called Thrust implements a dependent refinement type system plus an inference pipeline that emits Constrained Horn Clauses to a CHC solver… | ||
| Practical Type Inference with Levels | Andong Fan, Han Xu, Ningning Xie | 21m |
Formalizes the implementation trick called levels for Hindley‑Milner style systems, covering generalization, local data types, and higher‑rank polymorphism… | ||
| Dynamic Region Ownership for Concurrency Safety | Fridtjof Peer Stoldt, Brandt Bucher, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, Guido van Rossum, Eric Snow, Tobias Wrigstad | 18m |
Claims a runtime ownership model, Langfish, that enforces exclusive mutable access by grouping objects into regions and raising deterministic errors instead of… | ||
| Usability Barriers for Liquid Types | Catarina Gamboa, Abigail Elena Reese, Alcides Fonseca, Jonathan Aldrich | 19m |
Study reports a user study of LiquidHaskell with 12 novice and several experienced participants, yielding nine barriers across three concrete categories… | ||
| Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…) | Angus Hammond, Ricardo Almeida, Thomas Bauereiss, Brian Campbell, Ian Stark, Peter Sewell | 23m |
Proves that an encapsulated C-style component running on Arm Morello maintains a mod-64 accumulator invariant against arbitrary untrusted code, by mechanising… | ||
| Making Concurrent Hardware Verification Sequential | Thomas Bourgeat, Jiazheng Liu, Adam Chlipala | 21m |
Introduces Fjfj, a Bluespec-like language that removes exponential proof cases by separating action methods vs value methods and forbidding multiple action… | ||
| Ripple: Asynchronous Programming for Spatial Dataflow Architectures | Souradip Ghosh, Yufei Shi, Brandon Lucia, Nathan Beckmann | 21m |
Ripple is a new language plus ISA and microarchitectural support that exposes asynchronous iterators and hardware token queues so compilers lower queues and… | ||
| Program Skeletons for Automated Program Translation | Bo Wang, Tianyu Li, Ruishi Li, Umang Mathur, Prateek Saxena | 23m |
Proposes program skeletons that split a Python program into a mechanically converted skeleton and code fragments synthesized by LLMs, implements prototype SKEL… | ||
| DR.FIX: Automatically Fixing Data Races at Industry Scale | Farnaz Behrang, Zhizhou Zhang, Georgian-Vlad Saioc, Peng Liu, Milind Chabbi | 22m |
Dr.Fix combines program analysis with LLM-driven generation (GPT40) and a vector database of 272 past bug–fix examples to auto-propose patches for Go data… | ||
| Spineless Traversal for Layout Invalidation | Marisa Kirisame, Tiezhi Wang, Pavel Panchekha | 17m |
A new incremental-layout algorithm, Spineless Traversal, replaces top-down tree scans with a pointer queue ordered by order-maintenance timestamps to avoid… | ||
| An Interactive Debugger for Rust Trait Errors | Gavin Gray, Will Crichton, Shriram Krishnamurthi | 20m |
Argus visualizes Rust trait resolution as an interactive proof-search debugger with complementary bottom-up and top-down views, provenance paths, IDE… | ||
| Fast Direct Manipulation Programming with Patch-Reconciliation Correspondence | Parker Ziegler, Justin Lubin, Sarah E. Chasins | 20m |
Introduces a patch-recon architecture that pairs syntactic program patches with a semantic recon that directly updates map output (in-place updates of marks… | ||
| Dynamic Robustness Verification against Weak Memory | Roy Margalit, Michalis Kokologiannakis, Shachar Itzhaky, Ori Lahav | 17m |
Algorithm verifies robustness against C11/C++20 weak memory using location clocks and runs as the RSAN/Arson tool that reports full backtraces for violations… | ||
| Modular Construction and Optimization of the UZP Sparse Format for SpMV on CPUs | Alonso Rodríguez-Iglesias, Santoshkumar T. Tongli, Emily Tucker, Louis-Noël Pouchet, Gabriel Rodriguez, Juan Touriño | 23m |
Format encodes sparse coordinates as a union of integer polyhedra intersected with affine lattices so SpMV uses regular loops instead of index indirection, and… | ||
| Lightweight and Locality-Aware Composition of Black-Box Subroutines | Manya Bansal, Dillon Sharlet, Jonathan Ragan-Kelley, Saman Amarasinghe | 22m |
A system called Fern enriches black-box subroutine interfaces with producer-consumer annotations that describe how small data blocks are produced and consumed… | ||
| Task-Based Tensor Computations on Modern GPUs | Rohan Yadav, Michael Garland, Alex Aiken, Michael Bauer | 19m |
Cypress provides a task-based programming model that maps logical tensor tasks to Hopper GPU resources and lowers to CUDA that competes with handwritten code… | ||
| Handling the Selection Monad | Gordon Plotkin, Ningning Xie | 21m |
Designs effect handlers that expose loss continuations derived from the selection monad, letting handlers observe per-choice losses and resume computations… | ||
| A Modular Approach to Metatheoretic Reasoning for Extensible Languages | Dawn Michaelson, Gopalan Nadathur, Eric Van Wyk | 20m |
Claims a practical, sound method to build complete metatheory for languages assembled from independently written extensions by: decomposing proofs around… | ||
| First-Class Verification Dialects for MLIR | Mathieu Fehr, Yuyou Fan, Hugo Pompougnac, John Regehr, Tobias Grosser | 18m |
Adds semantics as first-class MLIR dialects and a pipeline that lowers compiler IRs through high-level memory and undefined-behavior dialects to an SMT… | ||
| MISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable(…) | Abdul Rafae Noor, Dhruv Baronia, Akash Kothari, Muchen Xu, Charith Mendis, Vikram S. Adve | 20m |
MISAAL is a synthesis-based compiler that moves expensive synthesis offline, uses instruction semantics to generate automated swizzle operators and… | ||
| Functional Meaning for Parallel Streaming | Nick Rioux, Steve Zdancewic | 19m |
A core language called λ∨ formalizes deterministic parallel streaming by making values monotonically increase under a streaming order that matches Scott… | ||
| Program Synthesis From Partial Traces | Margarida Ferreira, Victor Nicolet, Joey Dodds, Daniel Kroening | 21m |
A technique called Siren synthesizes API- and system-automation scripts from partial traces that record only side-effecting calls, combining compiler-style… | ||
| Multi-stage Relational Programming | Michael Ballantyne, Rafaello Sanna, Jason Hemann, William E. Byrd, Nada Amin | 16m |
Implements a multi-stage extension of miniKanren that compiles known parts of relational interpreters and defers unknown holes to a runtime relational… | ||
| Exact Loop Bound Analysis | Daniel Riley, Grigory Fedyukovich | 21m |
Tool computes exact iteration counts for single-loop Linear Integer Arithmetic programs by synthesizing precondition synthesis fragments and reducing each case… | ||
| A Concurrent Approach to String Transformation Synthesis | Yuantian Ding, Xiaokang Qiu | 18m |
Claims a first concurrent synthesis algorithm for string transformations that pairs an asynchronous deducer with a multi-request enumerator and uses an… | ||
| Programming by Navigation | Justin Lubin, Parker Ziegler, Sarah E. Chasins | 21m |
Defines Strong Completeness and Strong Soundness as showing all and only valid next edit steps, reduces synthesis to a type-inhabitation oracle, compiles types… | ||
| AWDIT: An Optimal Weak Database Isolation Tester | Lasse Møldrup, Andreas Pavlogiannis | 18m |
AWDIT implemented in Rust tests Read Committed, Read Atomic, and Causal Consistency with proven bounds O(n^{3/2}) for RC/RA, O(n·k) for CC, runs on histories… | ||
| Graphiti: Bridging Graph and Relational Database Queries | Yang He, Ruijie Fang, Işıl Dillig, Yuepeng Wang | 20m |
Builds an automated pipeline called Graphiti that encodes user mappings as a user-provided transformer, automatically derives a standard transformer, and… | ||
| Pointer Analysis for Database-Backed Applications | Yufei Liang, Teng Zhang, Ganlin Li, Tian Tan, Chang Xu, Chun Cao, Xiaoxing Ma, Yue Li | 19m |
DBridge is an end-to-end pointer analysis that constructs Java-to-database value flows for JDBC/Hibernate/Spring Data JPA apps, implemented as 14K LoC and… | ||
| Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search | Pinhan Zhao, Yuepeng Wang, Xinyu Wang | 20m |
Polygon implements a conflict-driven under-approximation search that encodes restricted SMT models of SQL operators (joins as matrices, filters as vectors) and… | ||
| Optimization-Directed Compiler Fuzzing for Continuous Translation Validation | Jaeseong Kwon, Bongjun Jang, Juneyoung Lee, Kihong Heo | 18m |
Optimuzz combines directed grey-box fuzzing with translation validation to find miscompilations; it targets optimization trigger locations, slices optimizer… | ||
| Divergence-Aware Testing of Graphics Shader Compiler Back-Ends | Dongwei Xiao, Shuai Wang, Zhibo Liu, Yiteng Peng, Daoyuan Wu, Zhendong Su | 21m |
ShaDiv generates shader tests that deliberately perturb control and data flow divergence to exercise backend optimizations, uses a divergence-aware generator… | ||
| Link-Time Optimization of Dynamic Casts in C++ Programs | Xufan Lu, Nuno P. Lopes | 22m |
Link-time pass turns library dynamic_cast calls into short instruction sequences by laying out classes in preorder layout bounds checks, replacing linear DFS… | ||
| CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…) | Ling Zhang, Yuting Wang, Yalun Liang, Zhong Shao | 19m |
Claim: a verified compiler that compositionally preserves semantics for cooperative multi-threaded C programs that share stack data. Key techniques are… | ||
| Robustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis | Shan Huang, Jingjing Liang, Ting Su, Qirun Zhang | 18m |
Tool MetaLoc instruments LLVM optimization passes, uses control-flow conformance analysis to infer correct debug-location updates, and emits patch skeletons… | ||
| Verifying Solutions to Semantics-Guided Synthesis Problems | Charlie Murphy, Keith J.C. Johnson, Thomas Reps, Loris D'Antoni | 18m |
Framework reduces SemGuS verification to reduction to µCLP and classifies problems into SMT-encodable, CHC-encodable, and µCLP-encodable cases, implements… | ||
| Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus | Steven Schaefer, Nathan Varner, Max S. New | 19m |
Presents LambekD, a dependent, ordered linear type theory that makes parsers sound by construction and, with a complement/disjointness proof, complete… | ||
| A Uniform Framework for Handling Position Constraints in String Solving | Yu-Fang Chen, Vojtěch Havlena, Michal Hečko, Lukáš Holík, Ondřej Lengál | 20m |
Introduces a decision procedure that avoids encoding to word equations and instead reduces position constraints to integer constraints extracted from the… | ||
| Verifying Lock-Free Traversals in Relaxed Memory Separation Logic | Sunho Park, Jaehwang Jung, Janggun Lee, Jeehoon Kang | 22m |
First mechanized verification of a lock-free linked list, skiplist, and skiplist-based priority queue against relaxed memory consistency, using the iRC11… | ||
| Destabilizing Iris | Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, Derek Dreyer | 22m |
Adds Daenerys to Iris: a reworked resource layer that introduces unstable resources and an explicit frame modality, plus an unstable points-to and a… | ||
| Certified Compilers à la Carte | Oghenevwogaga Ebresafe, Ian Zhao, Ende Jin, Arthur Bright, Charles Jian, Yizhou Zhang | 19m |
The work extends the Rocq proof assistant with a plugin called Rocqet that adds object-oriented extensibility features—late binding, mixin composition, and… | ||
| RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free(…) | Kimaya Bedarkar, Laila Elbeheiry, Michael Sammler, Lennard Gäher, Björn Brandenburg, Derek Dreyer, Deepak Garg | 18m |
Claims a machine‑checked end‑to‑end proof that an interrupt‑free, fixed‑priority, non‑preemptive scheduler meets response‑time bounds by connecting program… | ||
| A Hybrid Approach to Semi-automated Rust Verification | Sacha-Élie Ayoun, Xavier Denis, Petar Maksimovic, Philippa Gardner | 19m |
A prototype hybrid verifier links Gillian-Rust (symbolic-execution + separation logic) with Creusot so safe Rust specs are checked automatically while unsafe… | ||
| Membership Testing for Semantic Regular Expressions | Yifei Huang, Matin Amini, Alexis Le Glaunec, Konstantinos Mamouras, Mukund Raghothaman | 23m |
Presents a concrete two-pass NFA-based algorithm that converts a SemRE and input into a linear-size query graph then runs DP to check satisfiable paths… | ||
| Probabilistic Kleene Algebra with Angelic Nondeterminism | Shawn Ong, Stephanie Ma, Dexter Kozen | 18m |
Defines a Kleene-style algebra that combines probability with angelic nondeterminism by giving semantics as distributions over multisets to bypass the… | ||
| StacKAT: Infinite State Network Verification | Jules Jacobs, Nate Foster, Tobias Kappé, Dexter Kozen, Lily Saada, Alexandra Silva, Jana Wagemaker | 20m |
Defines StacKAT, a packet-language that adds a single variable-size stack payload with push/pop to NetKAT-style programs and proves program equivalence… | ||
| Active Learning of Symbolic NetKAT Automata | Mark Moeller, Tiago Ferreira, Thomas Lu, Nate Foster, Alexandra Silva | 18m |
Presents algorithms that learn symbolic NetKAT automata from active queries, proves soundness and termination, and ships a prototype implementation with… | ||
| Circuit Optimization using Arithmetic Table Lookups | Raghav Malik, Vedant Paranjape, Milind Kulkarni | 22m |
COATL is a compiler that replaces low-level Boolean gates with arithmetic lookup tables that index small-modulus ciphertexts and use ILP-synthesized… | ||
| Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…) | Owen Conoly, Andres Erbsen, Adam Chlipala | 23m |
Formal definition of cryptographic constant‑time for languages with compiler‑resolved nondeterminism using omnisemantics and single‑copy assertions, mechanized… | ||
| Robust Constant-Time Cryptography | Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan | 17m |
Defines an operational semantics and a new property Robust Constant Time (RCT) that is parameterized by attacker models (read gadgets, speculative read… | ||
| Automated Exploit Generation for Node.js Packages | Filipe Marques, Mafalda Sofia Ferreira, André Nascimento, Miguel E. Coimbra, Nuno Santos, Limin Jia, José Fragoso Santos | 20m |
Explode.js combines static analysis and lazy symbolic execution plus SMT solving to synthesize concrete exploits that reach vulnerable sinks through multi-call… | ||
| Verified Foundations for Differential Privacy | Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, Jean-Baptiste Tristan | 19m |
SampCert is a mechanized foundation for differential privacy written in Lean that proves correctness of sampling and DP composition and ships verified samplers… | ||
| Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs | Rudi Schneider, Marcus Rossel, Amir Shaikhha, Andrés Goens, Thomas Kœhler, Michel Steuwer | 20m |
E-graphs gain native support for bound variables by making e-classes functions over parameterized e-classes (slots) so alpha-equivalent terms share a single… | ||
| Webs and Flow-Directed Well-Typedness Preserving Program Transformations | Benjamin Quiring, David Van Horn, John Reppy, Olin Shivers | 20m |
Defines webs as connected components of a bipartite function‑call graph and ships a web-centric IR that annotates every function, call, and arrow type so… | ||
| Relaxing Alias Analysis: Exploring the Unexplored Space | Michel Weber, Theodoros Theodoridis, Zhendong Su | 20m |
This study instruments LLVM 17.0.6 and SPEC CPU 2017 and shows that removing alias analysis entirely changes final binaries only slightly on average, but only… | ||
| Exploiting Undefined Behavior in C/C++ Programs for Optimization: A Study on the(…) | Lucian Popescu, Nuno P. Lopes | 19m |
Demonstrates a large experiment using LLVM/Clang extensions to toggle 18 UB flags across 24 real applications (7M LOC) on Intel, AMD and ARM, measuring… | ||
| Partial Evaluation, Whole-Program Compilation | Chris Fallin, Maxwell Bernstein | 20m |
A tool called Weevil partial evaluator unrolls an SSA interpreter, uses context-sensitive constant propagation and memoized block copies to produce… | ||
| Memory-safe interoperation between safe and unsafe languages | Yeoul Na | 24m |
Describes a practical system that imports C/C++ pointers into Swift as a span safe pointer using counted_by and noescape annotations to encode bounds and… | ||
| An Overview of the Cangjie Language | Xinyu Feng | 22m |
Cangjie is a new statically typed, garbage‑collected language for HarmonyOS with an ARVM backend, stack‑based green threads with dynamic stack growth and a… | ||
| nothing matches | ||