1,971 papers · page 3 of 99
Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. For example, scope-based constructs like Java's synchronized blocks offer ease of reasoning, but they restrict expressiveness and para…
Reasoning about programs in the presence of mutation and aliasing is notoriously difficult. Rust has popu-larized lifetime-based ownership tracking in systems programming, but its “shared XOR mutable” model is fundamentally at odds with higher-level functional programming. Reacha…
Garbage collection (GC) remains a desirable yet elusive goal in unmanaged languages like C/C++ and Rust, where concurrent memory reclamation must be achieved without compiler or runtime support. Existing techniques face fundamental trade-offs among efficiency, safety, and ease of…
The CCR framework unifies refinement and separation logic to provide ownership-based modular reasoning and transitive incremental reasoning in open settings that involve unverified code. However, when reasoning about function invocations, the reasoning principles available to cli…
Users of program analyses expect that results change predictably in response to changes in their programs, but many analyses do not ensure such robustness. This paper introduces a theoretical framework that provides a unified language to articulate robustness properties. We adopt…
Despite the recent progress of automated program verification techniques, fully automated verification of programs manipulating recursive data structures remains a challenge. We introduce solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), novel formalisms for expressing…
Popular JVM-based search and analytics systems, such as Elasticsearch and Spark, rely on the OS page cache (I/O cache) to accelerate storage access. However, dividing memory between the JVM heap and the I/O cache creates a trade-off: enlarging the heap reduces garbage collection …
Equality saturation (eqsat) is a program optimization technique that uses syntax-based term rewriting to simultaneously explore many possible optimizations of a program, storing equivalent programs efficiently in a data structure called an e-graph. By exploring optimizations simu…
We propose new supermartingale-based certificates for verifying almost sure satisfaction of ω -regular properties: (1) generalised Streett supermartingales (GSSMs) and their lexicographic extension (LexGSSMs), (2) distribution-valued Streett supermartingales (DVSSMs), and (3) pro…
Many quantitative properties of probabilistic programs can be characterized as least fixed points, but verifying their lower bounds remains a challenging problem. We present a new approach to lower-bound verification that exploits and extends the connection between the uniqueness…
Inductive types are a fundamental abstraction mechanism in type theory and proof assistants, supporting the definition of data structures and rich specifications. Nested inductive types extend this mechanism by allowing constructors to use parametric types instantiated with the t…
The WebGPU programming model brings general-purpose GPU programming to the web, allowing untrusted JavaScript to issue parallel workloads to client GPUs. To ensure reliability, WebGPU mandates uniformity analysis —a static check that rejects programs that could cause barrier dive…
Specification-Driven Development (SDD) has emerged as a promising paradigm in software development. This trend is fueled by recent advances in leveraging large language models (LLMs) to generate code from user intents expressed in natural language. However, the reliance on natura…
WasmFX is a proposed extension of Wasm, a low-level portable bytecode, with primitives for explicitly manipulating execution stacks as continuations. By exposing an interface of effect handlers, WasmFX enables non-local control flow features to be compiled in a modular way: one h…
Implicits provide a powerful mechanism for term-based inference, where “obvious” arguments can be omitted and inferred by the type checker. This can greatly reduce the programmer’s burden and improve the clarity of expression. As such, many languages support a form of implicits i…
Dominance is a fundamental concept in compilers based on static single assignment (SSA) form. It underpins a wide range of analyses and transformations and defines a core property of SSA: every use must be dominated by its definition. We argue that this reliance on dominance has …
PriML, a language developed in recent work on responsive parallelism , extends traditional fine-grained parallel languages such as Cilk by allowing programmers to annotate threads with priorities . Programmers thus get the substantial throughput benefits of lightweight threads sc…
We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higherorder concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning principles from standard concurrent sepa…
Symbolic execution has emerged as a powerful technique for scaling exact probabilistic inference to languages with more expressive features. But, this expressivity comes at a price: probabilistic programming languages based on symbolic execution are difficult to debug, optimize, …
Iterators are a fundamental programming abstraction for traversing and modifying elements in containers in mainstream imperative languages such as C++ . Iterators provide a uniform access mechanism that hides low-level implementation details of the underlying data structure. Howe…