1,971 papers · page 2 of 99
We describe a comprehensive compilation approach for relational algebra, centered on an abstract loop-based intermediate representation (IR) that can express fused implementations of relational algebra operators on both sets and multisets. The loops are abstracted away from physi…
Abstract semantics has proven to be instrumental for accelerating search-based program synthesis, by enabling the sound pruning of a set of incorrect programs (without enumerating them). One may expect faster synthesis with increasingly finer-grained abstract semantics. Unfortuna…
Sparse matrix-vector multiplication (SpMV) is a crucial operation in scientific computing, graph analytics, and machine/deep learning. Its performance is highly sensitive to matrix sparsity patterns, necessitating tailored program designs. This paper introduces SparseZETA, an int…
We propose an incremental approach for safety proofs that decomposes a proof with a complex inductive invariant into a sequence of simpler proof steps. Our proof system combines rules for (i)~forward reasoning using inductive invariants, (ii)~backward reasoning using inductive in…
Representing bound variables in embedded languages is a challenging problem, often requiring painful tradeoffs between expressivity and usability. On the one hand, first-order representations using de Bruijn indices have many nice properties, but quickly become difficult to read …
Binary size reduction is an increasingly important optimization objective for compilers, especially in the context of mobile applications and resource-constrained embedded devices. In such domains, binary size often takes precedence over compilation time. One emerging technique t…
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. Efficient solutions to this problem are critica…
Current numerical abstract interpretation relies on fixed, hand-crafted, instruction-specific transformers tailored to each domain, giving rise to three significant limitations. First, extensibility is limited because transformers cannot be reused across domains and new transform…
Many important functional and security properties—including non-interference, determinism, and generalized non-interference (GNI)—are hyperproperties, i.e., properties relating multiple executions of a program. Existing separation logics allow one to reason about specific classes…
How to construct globally sound abstract interpreters to safely approximate program behaviors remains a bottleneck in abstract interpretation. In this paper, we show the potential of using state-of-the-art LLMs to automate this tedious process. Focusing on the neural network veri…
Taint analysis, widely used for bug and vulnerability detection, is typically formulated as a flow- and context-sensitive IFDS analysis. To achieve field sensitivity, IFDS models heap locations as k -limited access paths but suffers from cubic time and quadratic space complexity,…
Bounding volume hierarchies are ubiquitous acceleration structures in graphics, scientific computing, and data analytics. Their performance depends critically on data layout choices that affect cache utilization, memory bandwidth, and vectorization—increasingly dominant factors i…
We study the linearizability monitoring problem, which asks whether a given concurrent history of a data structure is equivalent to some sequential execution of the same data structure. In general, this problem is NP-hard, even for simple objects such as registers. Recent work ha…
Verus is a verification tool for the Rust programming language that has already been put to use in several significant systems verification efforts. Verus offers a distinctive approach among Rust verification systems in that, in addition to offering fast SMT-based automation, it …
Memory safety is traditionally characterized in terms of bad things that cannot happen. This approach is currently embraced in the literature on formal methods for memory safety. However, a general semantic principle for memory safety, that implies the negative items, remains elu…
Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially private algorithms is widely recognized and has sparked fruitful research on formal methods. Howeve…
Matching regexes (regular expressions) is a common problem in many areas of computer science, with requirements on high speed and robust performance. Regexes with backreferences allow one to express certain patterns (even beyond regular) concisely, however, since the matching is …
In functional data-parallel programs, index array computations are separated into sequences of bulk-parallel operators—map, prefix sum, scatter—and used to gather or scatter data array elements, thus determining data array properties. This programming style is problematic for gen…
Recent advances in foundation models have motivated hybrid programming that integrates natural language descriptions, formal specifications, and executable code. A critical challenge in such systems lies in achieving semantic alignment across heterogeneous representations at diff…
Matrix multiplication is a key operation in scientific computing and machine learning, with GPU libraries like NVIDIA Cutlass and cuBLAS providing optimized implementations of the three nested loop cubic algorithm. While sub-cubic algorithms, like the Strassen algorithm and its v…