Search events for 'all'
Enabling Huge Pages for Real-World Executables
ISMM 2026 People: Nadav Amit
… , and debugging all continue to work correctly. Hugifier combines a binary …
How Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler
SOAP When: Tue 16 Jun 2026 09:10 - 10:10 People: Yannis Smaragdakis
… decompilation can really be a "what will the program do for all inputs …
Exploring Locally Bounded Translation Validation
SOAP When: Tue 16 Jun 2026 10:30 - 10:50 People: Alborz Jelvani, Richard P. Martin, Santosh Nagarakatte
… Bounded translation validation (TV) is a common method used to check for the equivalence of two programs by unrolling all loops according to a user-supplied global bound. Unfortunately, large unroll bounds with multiple loops can …
Rhyme: A Multi-Paradigm Declarative Query Language
ARRAY 2026 When: Tue 16 Jun 2026 15:00 - 15:20 People: Ran Guo, Tiark Rompf
… diverse computations such as tensor calculations can all be expressed in a unified …
Relational E-matching in an SMT solver
EGRAPHS People: Amar Shah, Marijn Heule, Bryan Parno, Max Willsey
… E-matching is the problem of finding all matches of a pattern in an e-graph. Relational e-matching, a recent approach inspired by the databases community, has found succcess in equality saturation engines such as egglog. However, until …
Compile-Time Java Stream Fusion via mapMulti
SOAP When: Tue 16 Jun 2026 11:10 - 11:30 People: Yegor Bugayenko, Maxim Trunnikov, Vladimir Zakharov
… also applied it to the bytecode of Apache Kafka, successfully executing all 31,799 …
A Pointer-Ownership Model for C Inspired by Rust
LCTES 2026 When: Tue 16 Jun 2026 11:12 - 11:34 People: David Svoboda, William Klieber, Lori Flynn, Ruben Martins, Jeffrey Hoskinson
… test suite of memory-safe and memory-unsafe code examples. We tested all 4,604 …, 415, 416, 590, 761) from the Juliet C/C++ test suite. In our tests, all …
Relational Cell Morphing: Automated Verification of Relational Properties of Array Programs
ARRAY 2026 When: Tue 16 Jun 2026 10:50 - 11:15 People: Weihao Qu, Marco Gaboardi, Hiroshi Unno, Eric Koskinen
… 8 property classes, all verified in seconds to minutes by PCSat. …
Graded Monoids for Dependently Typed Array Programming
ARRAY 2026 When: Tue 16 Jun 2026 11:15 - 11:40 People: Juuso Haavisto, Jeremy Gibbons
… .
Specifically, in an array language where all operations are folds, folding …
Tensor Algebra Equivalence Checker
ARRAY 2026 When: Tue 16 Jun 2026 14:40 - 15:00 People: Jubi Taneja, Tom St. John, Natalie Serrino
… baseline for \emph{all} inputs. The equivalence checker lowers both programs through …
Semantics as a Tool of Thought: Provenance-Aware Dimensional Checking in a Reactive Array IR
ARRAY 2026 When: Tue 16 Jun 2026 17:15 - 17:20 People: Christopher Buck
… at 60fps. A 26-case judgment suite validates all four judgment forms; median …
Sirop: A Small IR for HLS with Parallel Patterns
LCTES 2026 When: Tue 16 Jun 2026 14:22 - 14:44 People: Louis Hildebrand, Christophe Dubach
… the Intel HLS compiler, all for the same throughput. …
Hikami: A Lightweight Hypervisor for Emulating RISC-V Extension Semantics with Sail-Driven Auto-generation
LCTES 2026 When: Tue 16 Jun 2026 11:34 - 11:56 People: Norimasa Takana, Yoshihiro Oyama
… system allows guest software to run natively for all supported instructions …
Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows
PLDI Research Papers When: Wed 17 Jun 2026 11:30 - 11:50 People: Zain K Aamer, Rini Banerjee, Hiroyuki Katsura, David Kaloper-Meršinjak, Dimitrios J. Economou, Kayvan Memarian, Dhruv Makwana, Neel Krishnaswami, Benjamin C. Pierce, Christopher Pulte, Peter Sewell
… —and how each of these complements and supports the others. We demonstrate all …
Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity
PLDI Research Papers When: Wed 17 Jun 2026 15:00 - 15:20 People: Jiayi Wang, Yu Wang, Linzhang Wang, Ke Wang
… is independent of program inputs along each execution path, then once all such paths from …-agnostic alarms among all reported alarms. However, validating even input-agnostic alarms requires exploring all feasible paths, which is generally infeasible …
An Efficient Algorithm for Streaming BPE Tokenization
PLDI Research Papers When: Thu 18 Jun 2026 10:50 - 11:10 People: Konstantinos Mamouras, Angela W. Li, Yudi Yang
… Tokenization is an essential text preprocessing step in almost all large language models (LLMs), and byte-pair encoding (BPE) is a popular tokenization method used by models such as GPT, GPT-2, and RoBERTa. Since LLMs have many …
Fast Atomicity Monitoring
PLDI Research Papers When: Wed 17 Jun 2026 14:40 - 15:00 People: Hünkar Can Tunç, Yifan Dong, Andreas Pavlogiannis
… in an efficient streaming style, is theoretically faster than all existing algorithms …{AtomSanitizer} is always faster in practice than all existing conflict …
Bonsai: Compiling Queries to Pruned Tree Traversals
PLDI Research Papers When: Fri 19 Jun 2026 16:10 - 16:30 People: Alexander J Root, Christophe Gyurgyik, Purvi Goel, Kayvon Fatahalian, Jonathan Ragan-Kelley, Andrew Adams, Fredrik Kjolstad
… Trees can accelerate queries that search or aggregate values over large collections. They achieve this by storing metadata that enables quick pruning (or inclusion) of subtrees when predicates on that metadata can prove that none (or all …
Path-Sensitive Abstract Interpretation for WCET Estimation
PLDI Research Papers When: Wed 17 Jun 2026 15:50 - 16:10 People: Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, Lei Ju
… abstract interpretation to estimate cache behaviors without enumerating all paths …
The Search for Constrained Random Generators
PLDI Research Papers When: Thu 18 Jun 2026 14:40 - 15:00 People: Harrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati, Leonidas Lampropoulos, Benjamin C. Pierce
… Among the biggest challenges in property-based testing (PBT) is the constrained random generation problem: given a predicate on program values, randomly sample from the set of all values, and only values, satisfying that predicate …
Virtualizing Continuations
PLDI Research Papers When: Fri 19 Jun 2026 16:50 - 17:10 People: Cong Ma, Jonghyun Jung, Yizhou Zhang
… instance is assigned a virtual address, and all effect invocations through …
Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
PLDI Research Papers When: Wed 17 Jun 2026 11:10 - 11:30 People: Rui Dong, Qingyue Wu, Danny Ding, Zheng Guo, Ruyi Ji, Xinyu Wang
… manipulation. All of them significantly outperform prior work in the respective …
[SIGPLAN] Active Learning for Neurosymbolic Program Synthesis
PLDI Research Papers When: Fri 19 Jun 2026 16:50 - 17:10 People: Celeste Barnaby, Jocelyn Qiaochu Chen, Ramya Ramalingam, Osbert Bastani, Işıl Dillig
… . Our proposed method iteratively makes CCE more precise until all remaining …
Fungible Memories for Automated Technology Mapping and Retargeting
PLDI Research Papers When: Thu 18 Jun 2026 14:40 - 15:00 People: Zachary D. Sisco, Sijie Kong, Daniel Ruelas-Petrisko, Jingtao Xia, Julian Springer, Varun Rao, Spencer Wang, Gus Henry Smith, Ben Hardekopf, Jonathan Balkind
… semantics to automatically target all relevant technologies using a single generic …
VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System
PLDI Research Papers When: Fri 19 Jun 2026 14:40 - 15:00 People: Travis Hance, Laila Elbeheiry, Yusuke Matsushita, Derek Dreyer
… with the Leaf library for temporary resource sharing in Iris. All our proofs …
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
PLDI Research Papers When: Thu 18 Jun 2026 13:40 - 14:00 People: Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
… }$ function of the Sodium cryptography software library.
All results have …
Backwards-Compatible Row-Based Exceptions in ML
PLDI Research Papers When: Wed 17 Jun 2026 16:30 - 16:50 People: Simcha van Collem, Paulo Emílio de Vilhena, Robbert Krebbers
… thesis. All our results are mechanized in the Rocq prover using Iris. …
Enumerating Ill-Typed Programs for Testing Type Analyzers
PLDI Research Papers People: Thodoris Sotiropoulos, Zhendong Su
… We propose error enumeration, a method that aims to discover soundness defects in type analyzers by generating ill-typed programs by construction. Given a well-typed program $P$, it systematically injects type mismatches at all possible …
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
PLDI Research Papers When: Fri 19 Jun 2026 11:50 - 12:10 People: Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf
… }—avoiding ill-scoped names in types.
With all prior works being declarative,
we …
Uniformity Analysis in the WebGPU Shading Language
PLDI Research Papers When: Wed 17 Jun 2026 17:10 - 17:30 People: James Lee-Jones, John Wickerson, Alastair F. Donaldson
… significant changes to the specification (all accepted).
%
(4) \emph{Testing …
Towards Removing Undef Values from LLVM IR
PLDI Research Papers When: Thu 18 Jun 2026 10:30 - 10:50 People: Pedro Lobo, John McIver, George Mitenkov, Juneyoung Lee, Kirshanthan Sundararajah, Nuno P. Lopes
… and optimizations for the regular cases is already tricky; ensuring that these are sound for all …
Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
PLDI Research Papers When: Wed 17 Jun 2026 16:30 - 16:50 People: Shaurya Gomber, Debangshu Banerjee, Gagandeep Singh
… . Third, all downstream tasks are forced to use the same fixed transformer …
SuperCollider: Scalable and Effective Data Race Detection for CUDA
PLDI Research Papers When: Wed 17 Jun 2026 14:20 - 14:40 People: Mark Stephenson, Sana Damani, Mohamed Tarek Ibn Ziad, Anis Ladram, Michael Garland
… SuperCollider cannot detect all races, we demonstrate that it effectively catches …
Parameterized Algorithms and Complexity for Function Merging with Branch Reordering
PLDI Research Papers When: Fri 19 Jun 2026 10:50 - 11:10 People: Amir K. Goharshady, Kerim Kochekov, Tian Shu, Ahmed Khaled Zaher
… that the problem is fixed-parameter tractable (FPT) with respect to all four …
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
PLDI Research Papers When: Fri 19 Jun 2026 13:40 - 14:00 People: Samuel Teuber, Mattias Ulbrich, André Platzer, Bernhard Beckert
… and combination, and prove the soundness of all proof rules in Isabelle. We …
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
PLDI Research Papers When: Thu 18 Jun 2026 14:40 - 15:00 People: Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, Lars Birkedal
… of our library. All of our results have been foundationally verified in the Rocq …
Pantomime: Constructive Leakage Proofs via Simulation
PLDI Research Papers When: Thu 18 Jun 2026 11:50 - 12:10 People: Robin Webbers, Robert Schenck, Wind Wong, Kristina Sojakova, Klaus von Gleissenthall
… hardware design that must faithfully replicate all attacker-observable behavior from …
SIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior
PLDI Research Papers When: Wed 17 Jun 2026 16:50 - 17:10 People: Zheyuan Chen, Naomi Rehman, Guido Martínez, Tyler Sorensen
… of the idiomatic tests, all of which can be verified in under one second …
State Space Estimation for DPOR-Based Model Checkers
PLDI Research Papers When: Wed 17 Jun 2026 13:40 - 14:00 People: A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur, Minjian Zhang
… also show how the same machinery estimates model-checking cost by weighting all …
[SIGPLAN] Complete the Cycle: Reachability Types with Expressive Cyclic References
PLDI Research Papers When: Wed 17 Jun 2026 16:10 - 16:30 People: Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
… a qualifier must include all transitively reachable locations, reducing precision …
[SIGPLAN] Probabilistic Refinement Session Types
PLDI Research Papers When: Wed 17 Jun 2026 15:50 - 16:10 People: Qiancheng Fu, Ankush Das, Marco Gaboardi
… constructors. Unfortunately, all the proposed extensions only support constant …
SSA without Dominance for Higher-Order Programs
PLDI Research Papers When: Wed 17 Jun 2026 14:00 - 14:20 People: Roland Leißa, Johannes Griebler
… that all uses of a variable must be dominated by its definition loses meaning …
Scalable Floating-Point Satisfiability via Staged Optimization
PLDI Research Papers When: Thu 18 Jun 2026 11:10 - 11:30 People: Yuanzhuo Zhang, Zhoulai Fu, Binoy Ravindran
… if and only if a candidate satisfies all constraints. Thus, whenever optimization …
Exploiting Sophisticated Static Analysis for Verilog
PLDI Research Papers When: Wed 17 Jun 2026 14:40 - 15:00 People: Qinlin Chen, Nairen Zhang, Jinpeng Wang, Jiacai Cui, Tian Tan, Xiaoxing Ma, Chang Xu, Jian Lu, Yue Li
… + GitHub stars) uncovered nine previously unknown bugs, all confirmed …