Search events for 'all'
Informal Workshop Dinner (at SALT)
PROPL 2026 When: Mon 15 Jun 2026 19:00 - 21:00
… We will have an informal workshop dinner at SALT, located at 1047 Pearl Street, at 7pm. All are welcome, pay your own way. …
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 …
Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
PAgE 2026 When: Mon 15 Jun 2026 11:20 - 11:40 People: Martin C. Rinard
… This paper presents the use of testing, credible compilation/translation validation, verification, and audits in the Axon compiler. Axon comes with fully machine checked proofs that guarantee the correctness of the generated code. All code …
Exploring Locally Bounded Translation Validation
SOAP When: Tue 16 Jun 2026 10:40 - 11:00 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 …
Combining Agentic AI and Lightweight Formal Methods To Find Bugs in a Production Hypervisor
PAgE 2026 When: Mon 15 Jun 2026 13:40 - 14:00 People: Hiroyuki Katsura, Kayvan Memarian, Peter Sewell
… leakage or hypervisor memory corruption. Interestingly, all the bugs claimed …
Compile-Time Java Stream Fusion via mapMulti
SOAP When: Tue 16 Jun 2026 11:20 - 11:40 People: Yegor Bugayenko, Maxim Trunnikov, Vladimir Zakharov
… also applied it to the bytecode of Apache Kafka, successfully executing all 31,799 …
Enabling Huge Pages for Real-World Executables
ISMM 2026 When: Tue 16 Jun 2026 15:50 - 16:15 People: Nadav Amit
… , and debugging all continue to work correctly. Hugifier combines a binary …
The Next Frontier for AI-Generated Kernels: Correctness
PAgE 2026 When: Mon 15 Jun 2026 11:40 - 12:00 People: Guido Martínez, Tyler Sorensen
… verified GPU programming framework, we present verified implementations for all 100 …
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 When: Mon 15 Jun 2026 15:50 - 16:15 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 …
Agentic Code Reasoning
PAgE 2026 When: Mon 15 Jun 2026 10:40 - 11:00 People: Shubham Ugare, Satish Chandra
… improves accuracy on all of them. For patch equivalence, accuracy improves from 78 …
A Pointer-Ownership Model for C Inspired by Rust
LCTES 2026 When: Tue 16 Jun 2026 11:02 - 11:24 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 …
Graded Monoids for Dependently Typed Array Programming
ARRAY 2026 When: Tue 16 Jun 2026 11:25 - 11:45 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 …
Relational Cell Morphing: Automated Verification of Relational Properties of Array Programs
ARRAY 2026 When: Tue 16 Jun 2026 11:05 - 11:25 People: Weihao Qu, Marco Gaboardi, Hiroshi Unno, Eric Koskinen
… 8 property classes, all verified in seconds to minutes by PCSat. …
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:02 - 14:24 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:24 - 11:46 People: Norimasa Takana, Yoshihiro Oyama
… system allows guest software to run natively for all supported instructions …
URM Lunch
Diversity, Equity and Inclusion When: Fri 19 Jun 2026 12:40 - 14:00
… The URM@PLDI lunch will be held on Friday, June 19 with the goal of bringing together all who are under-represented within the SIGPLAN community. Lunch … is explicitly intended to be a “big tent” event, and is open to all who are under …
Formal Methods for Securing Federated Authorization: A Case Study of SciTokens
Student Research Competition When: Wed 17 Jun 2026 17:50 - 19:30 People: Minh Le
… consider all edge cases that often escape manual auditing and testing. …
Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows
PLDI Research Papers When: Wed 17 Jun 2026 12:00 - 12:20 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 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 …
Scenario-based Proof for Distributed Protocols
Student Research Competition When: Wed 17 Jun 2026 17:50 - 19:30 People: Zhendong Ang
… }, that the scenario’s commutativity closure contains all protocol executions, and \emph …
An Efficient Algorithm for Streaming BPE Tokenization
PLDI Research Papers When: Thu 18 Jun 2026 11:20 - 11:40 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 …
PLDI Business Meeting
PLDI Events When: Thu 18 Jun 2026 18:00 - 19:00
… encourage all to attend the business meeting and share their thoughts on how we …
Fast Atomicity Monitoring
PLDI Research Papers When: Wed 17 Jun 2026 15:00 - 15:20 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 …
E-Graph-Based Metamorphic Testing for Datalog Engines
Student Research Competition When: Wed 17 Jun 2026 17:50 - 19:30 People: Samuel Gerbers
… observed code coverage across all evaluated source test-case generation methods …
Automatic Energy Analysis Using Types
Student Research Competition When: Wed 17 Jun 2026 17:50 - 19:30 People: Sai Divvela
… techniques that reason over all possible program executions.
However …
Implementing Hybrid Resource Analysis in Resource Aware ML 2
Student Research Competition When: Wed 17 Jun 2026 17:50 - 19:30 People: Arnav Sabharwal
… analyzed over all inputs. AARA excels at deriving tight worst-case bounds …
Towards Taming Indirect Control Flow in Binaries with Multi-Task Graph Learning
Student Research Competition When: Wed 17 Jun 2026 17:50 - 19:30 People: Kun Liu
… , a unified multi-task learning framework designed to resolve all major ICF variants …
Women's Dinner
Diversity, Equity and Inclusion When: Wed 17 Jun 2026 19:30 - 21:30
… , and trans individuals of all stripes who find fellowship in women-centered …
Bonsai: Compiling Queries to Pruned Tree Traversals
PLDI Research Papers When: Fri 19 Jun 2026 16:30 - 16:50 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 …
Virtualizing Continuations
PLDI Research Papers When: Fri 19 Jun 2026 17:10 - 17:30 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:40 - 12:00 People: Rui Dong, Qingyue Wu, Danny Ding, Zheng Guo, Ruyi Ji, Xinyu Wang
… manipulation. All of them significantly outperform prior work in the respective …
Backwards-Compatible Row-Based Exceptions in ML
PLDI Research Papers When: Wed 17 Jun 2026 16:50 - 17:10 People: Simcha van Collem, Paulo Emílio de Vilhena, Robbert Krebbers
… thesis. All our results are mechanized in the Rocq prover using Iris. …
[SIGPLAN OOPSLA’25] Active Learning for Neurosymbolic Program Synthesis
PLDI Research Papers When: Fri 19 Jun 2026 16:30 - 16:50 People: Celeste Barnaby, Jocelyn Qiaochu Chen, Ramya Ramalingam, Osbert Bastani, Işıl Dillig
… . Our proposed method iteratively makes CCE more precise until all remaining …
Path-Sensitive Abstract Interpretation for WCET Estimation
PLDI Research Papers People: Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, Lei Ju
… abstract interpretation to estimate cache behaviors without enumerating all paths …
Fungible Memories for Automated Technology Mapping and Retargeting
PLDI Research Papers When: Thu 18 Jun 2026 15:00 - 15:20 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 15:00 - 15:20 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 14:00 - 14:20 People: Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
… }$ function of the Sodium cryptography software library.
All results have …
The Search for Constrained Random Generators
PLDI Research Papers When: Thu 18 Jun 2026 15:00 - 15:20 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 …
Towards Removing Undef Values from LLVM IR
PLDI Research Papers When: Thu 18 Jun 2026 11:00 - 11:20 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 …
SuperCollider: Scalable and Effective Data Race Detection for CUDA
PLDI Research Papers When: Wed 17 Jun 2026 14:40 - 15:00 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 11:20 - 11:40 People: Amir K. Goharshady, Kerim Kochekov, Tian Shu, Ahmed Khaled Zaher
… that the problem is fixed-parameter tractable (FPT) with respect to all four …
Pantomime: Constructive Leakage Proofs via Simulation
PLDI Research Papers When: Thu 18 Jun 2026 12:20 - 12:40 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 17:10 - 17:30 People: Zheyuan Chen, Naomi Rehman, Guido Martínez, Tyler Sorensen
… the behavior 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 14:00 - 14:20 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 OOPSLA’25] Complete the Cycle: Reachability Types with Expressive Cyclic References
PLDI Research Papers When: Wed 17 Jun 2026 16:30 - 16:50 People: Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
… a qualifier must include all transitively reachable locations, reducing precision …
SSA without Dominance for Higher-Order Programs
PLDI Research Papers When: Wed 17 Jun 2026 14:20 - 14:40 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:40 - 12:00 People: Yuanzhuo Zhang, Zhoulai Fu, Binoy Ravindran
… if and only if a candidate satisfies all constraints. Thus, whenever optimization …
Uniformity Analysis in the WebGPU Shading Language
PLDI Research Papers When: Wed 17 Jun 2026 17:30 - 17:50 People: James Lee-Jones, John Wickerson, Alastair F. Donaldson
… significant changes to the specification (all accepted).
%
(4) \emph{Testing …
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
PLDI Research Papers When: Thu 18 Jun 2026 15:00 - 15:20 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 …
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
PLDI Research Papers When: Fri 19 Jun 2026 14:00 - 14:20 People: Samuel Teuber, Mattias Ulbrich, André Platzer, Bernhard Beckert
… and combination, and prove the soundness of all proof rules in Isabelle. We …
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
PLDI Research Papers When: Fri 19 Jun 2026 12:20 - 12:40 People: Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf
… }—avoiding ill-scoped names in types.
With all prior works being declarative,
we …
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 …
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 …
[SIGPLAN PLDI’25] Probabilistic Refinement Session Types
PLDI Research Papers When: Wed 17 Jun 2026 16:10 - 16:30 People: Qiancheng Fu, Ankush Das, Marco Gaboardi
… constructors. Unfortunately, all the proposed extensions only support constant …
Exploiting Sophisticated Static Analysis for Verilog
PLDI Research Papers When: Wed 17 Jun 2026 15:00 - 15:20 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 …