Search events for 'all'
Accelerating the Static Analysis of Neural Networks by Batch Representation of Abstract Values
ARRAY 2025 People: Guillaume Berthelot, Arnault Ioualalen, Matthieu Martel
… Deep Neural Networks (DNNs) are increasingly being used in mission-critical systems. However, their use poses significant safety challenges and requires rigorous verification to ensure their correctness in all scenarios. Formal …
Gate Fusion is Map Fusion
ARRAY 2025 People: Martin Elsman, Troels Henriksen
… Most efficient state-vector quantum simulation frameworks are imperative. They work by having circuit gates operate on the global state vector in sequence and with each gate operation accessing and updating, in parallel, all (or large …
Optimization and Synthesis of Quantum Circuits with Global Gates
WQS 2025 When: Tue 17 Jun 2025 14:40 - 15:00 People: Alejandro Villoria, Henning Basold, Alfons Laarman
… , while on a trapped ion quantum computer, the connectivity is all-to-all. This all-to-all connectivity naturally gives us a special set of quantum gates to work …
Towards Bit-Level Dominance Preserving Quantization of Neural Classifiers
State Of the Art in Program Analysis When: Mon 16 Jun 2025 16:40 - 17:00 People: Dorra Ben Khalifa, Matthieu Martel
… and the proposed quantization holds for all the inputs. Technically, we use …
Machine Learning Guided Equality Saturation
EGRAPHS 2025 When: Tue 17 Jun 2025 16:00 - 16:20 People: Nicole Heinimann, Thomas Koehler, Michel Steuwer
… Equality saturation has successfully been applied in many domains. Yet, scaling issues hold back its success in even more applications. The underlying e-graph data structure can grow rapidly quickly consuming all available resources …
Beyond Affine Loops: A Geometric Approach to Program Synthesis
State Of the Art in Program Analysis When: Mon 16 Jun 2025 11:30 - 11:50 People: Erdenebayar Bayarmagnai, Fatemeh Mohammadi, Rémi Prébet
… correspond to all loops satisfying the given polynomial invariants. In other words …
Reworking Memory Management in CRuby: A Practitioner Report
ISMM 2025 When: Tue 17 Jun 2025 11:00 - 11:20 People: Kunshan Wang, Stephen M. Blackburn, Peter Zhu, Matthew Valentine-House
… objects, falling back to malloc to manage all larger objects. This paper …
Reconsidering Garbage Collection in Julia: A Practitioner Report
ISMM 2025 When: Tue 17 Jun 2025 10:40 - 11:00 People: Luis Eduardo de Souza Amorim, Yi Lin, Stephen M. Blackburn, Diogo Netto, Gabriel Baraldi, Nathan Daly, Tony Hosking, Kiran Pamnany, Oscar Smith
… Julia is a dynamically typed garbage collected language designed for high performance. Julia has a non-moving tracing collector, which while performant, is subject to the same unavoidable fragmentation and lack of locality of all other …
Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
PLDI Research Papers When: Fri 20 Jun 2025 14:00 - 14:20 People: Pinhan Zhao, Yuepeng Wang, Xinyu Wang
… -approximations (which collectively cover all program behaviors of interest … that Polygon significantly outperforms all prior techniques. …
Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
PLDI Research Papers When: Thu 19 Jun 2025 11:50 - 12:10 People: Sunho Park, Jaehwang Jung, Janggun Lee, Jeehoon Kang
… causality, rather than a total order of all operations. (2) <em …. All our proofs are mechanized on the iRC11 relaxed memory separation logic, built …
Solving Floating-Point Constraints with Continuous Optimization
PLDI Research Papers When: Wed 18 Jun 2025 14:00 - 14:20 People: Qian Chen, Chenqi Cui, Fengjuan Gao, Yu Wang, Ke Wang, Linzhang Wang
…
all benchmarks. It is worth mentioning that \textsf{Bitwuzla} and \textsf …, they have won all gold medals
for \textit{QF_FPArith} and \textit{FPArith … the source code of \textsf{Grater}, along with all evaluation data,
including …
Efficient, Portable, Census-Polymorphic Choreographic Programming
PLDI Research Papers When: Thu 19 Jun 2025 14:40 - 15:00 People: Mako P. Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, Joseph P. Near
… Choreographic programming (CP) is a paradigm for implementing distributed systems that uses a single global program to define the actions and interactions of all participants. Library-level CP implementations, like HasChor, integrate …
Webs and Flow-Directed Well-Typedness Preserving Program Transformations
PLDI Research Papers When: Wed 18 Jun 2025 11:30 - 11:50 People: Benjamin Quiring, David Van Horn, John Reppy, Olin Shivers
… languages, multiple functions can flow to the same call, all of which must agree …) transformations guided by these annotations. As they affect all members of a web …
CRGC: Fault-Recovering Actor Garbage Collection in Pekko
PLDI Research Papers When: Fri 20 Jun 2025 11:30 - 11:50 People: Dan Plyukhin, Gul Agha, Fabrizio Montesi
… tolerance, but resource management remains challenging: in all four of the most …-garbage actors are never killed) and completeness (all garbage actors are eventually …
Robustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis
PLDI Research Papers When: Fri 20 Jun 2025 10:30 - 10:50 People: Shan Huang, Jingjing Liang, Ting Su, Qirun Zhang
… reported and patched 46 previously unknown update errors in LLVM. All the patches …, effectively improving the accuracy and reliability of debug information in all …
Principal Type Inference under a Prefix: A Fresh Look at Static Overloading
PLDI Research Papers When: Thu 19 Jun 2025 14:20 - 14:40 People: Daan Leijen, Wenjia Ye
… a most general type that encompasses all possible derivations – Algorithm W … to specify as a logical deduction rule though, as it ranges over all possible …
First-Class Verification Dialects for MLIR
PLDI Research Papers When: Wed 18 Jun 2025 14:40 - 15:00 People: Mathieu Fehr, Yuyou Fan, Hugo Pompougnac, John Regehr, Tobias Grosser
… —optimizers, analyzers, verifiers, transformers—must all be engineered by hand …
in all executions) and “demanded bits” (that finds donot-care bits). The transfer …
Robust Constant-Time Cryptography
PLDI Research Papers When: Wed 18 Jun 2025 14:40 - 15:00 People: Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan
… for all contexts: a chosen protection could impose unnecessary overheads … making one-size-fits-all choices between security and performance. …
Unlocking Optimizations with egglog: Equality Saturation Meets Datalog
Tutorials People: Haobin Ni, Yihong Zhang, Zachary Tatlock, Oliver Flatt
… system.
egglog for Everyone
This tutorial welcomes all researchers …
Functional Meaning for Parallel Streaming
PLDI Research Papers When: Wed 18 Jun 2025 14:00 - 14:20 People: Nick Rioux, Steve Zdancewic
… to a \emph{streaming order} and all computations are monotone with respect …
Program Synthesis From Partial Traces
PLDI Research Papers When: Wed 18 Jun 2025 11:50 - 12:10 People: Margarida Ferreira, Victor Nicolet, Joey Dodds, Daniel Kroening
… , or a script from traces of system calls made by a workload, for example. All …
Spineless Traversal for Layout Invalidation
PLDI Research Papers When: Thu 19 Jun 2025 11:10 - 11:30 People: Marisa Kirisame, Tiezhi Wang, Pavel Panchekha
… ,
and are responsible for a sizable fraction
of all layout latency.
We …
An Interactive Debugger for Rust Trait Errors
PLDI Research Papers When: Thu 19 Jun 2025 10:50 - 11:10 People: Gavin Gray, Will Crichton, Shriram Krishnamurthi
… the traditional model of compiler diagnostics as one-size-fits-all, instead providing …
Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses
PLDI Research Papers When: Fri 20 Jun 2025 14:40 - 15:00 People: Fabian Stemmler, Michael Schwarz, Julian Erhard, Sarah Tilscher, Helmut Seidl
… and querying their values. Usually, all contributions
to globals are accumulated during …
Destabilizing Iris
PLDI Research Papers When: Thu 19 Jun 2025 11:30 - 11:50 People: Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, Derek Dreyer
… The separation logic framework Iris has been built on the premise that all assertions are \emph{stable}, meaning they unconditionally enjoy the famous \emph{frame rule}. This gives Iris—and the numerous program logics that build …
Programming by Navigation
PLDI Research Papers When: Wed 18 Jun 2025 10:30 - 10:50 People: Justin Lubin, Parker Ziegler, Sarah E. Chasins
… all valid next steps (Strong Completeness) and only valid next steps …
Task-Based Tensor Computations on Modern GPUs
PLDI Research Papers When: Wed 18 Jun 2025 16:00 - 16:15 People: Rohan Yadav, Michael Garland, Alex Aiken, Michael Bauer
… -known Flash Attention implementation while eliminating all aspects of explicit data …
Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus
PLDI Research Papers When: Thu 19 Jun 2025 14:20 - 14:40 People: Steven Schaefer, Nathan Varner, Pedro Henrique Azevedo de Amorim, Max S. New
… a shallow embedding in the Agda proof assistant. All of our examples parsers have …
LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols
PLDI Research Papers When: Fri 20 Jun 2025 14:20 - 14:40 People: Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, Zhong Shao
… and liveness proofs for all three protocols, which are also the first mechanized …
Pointer Analysis for Database-Backed Applications
PLDI Research Papers When: Fri 20 Jun 2025 14:20 - 14:40 People: Yufei Liang, Teng Zhang, Ganlin Li, Tian Tan, Chang Xu, Chun Cao, Xiaoxing Ma, Yue Li
… broken access control vulnerabilities, all previously undiscovered and real, as well …
Semantics of Integrating and Differentiating Singularities
PLDI Research Papers When: Wed 18 Jun 2025 10:50 - 11:10 People: Jesse Michel, Wonyeol Lee, Hongseok Yang
… define the denotational semantics of \textsc{SingularFlow}, deriving all …
Program Skeletons for Automated Program Translation
PLDI Research Papers When: Thu 19 Jun 2025 11:50 - 12:10 People: Bo Wang, Tianyu Li, Ruishi Li, Umang Mathur, Prateek Saxena
… be automatically translated, while about $5$% require manual effort. All the final …
Probabilistic Refinement Session Types
PLDI Research Papers When: Wed 18 Jun 2025 11:10 - 11:30 People: Qiancheng Fu, Ankush Das, Marco Gaboardi
… constructors. Unfortunately, all the proposed extensions only support constant …
Random Variate Generation with Formal Guarantees
PLDI Research Papers When: Wed 18 Jun 2025 10:30 - 10:50 People: Feras Saad, Wonyeol Lee
… Generating random variates is a fundamental operation in diverse areas of computer science and is supported in almost all modern programming languages. Traditional software libraries for random variate generation are grounded …
BINSEC: Adapting Symbolic Execution for Binary-level Security
Workshops and Tutorials People: Frédéric Recoules, Sébastien Bardin
… . ESOP 2023.
- Guillaume Girol, Benjamin Farinier, and Sébastien Bardin. Not all …
BINSEC: Adapting Symbolic Execution for Binary-level Security
Tutorials People: Frédéric Recoules, Sébastien Bardin
… Bardin. Not all bugs are created equal, but robust reachability can tell …