7,482 papers · page 9 of 375
Decidable automation is a key feature of program verification tools, which makes them easier for non-expert developers to use and understand. Unfortunately, decidable fragments of logic are very restrictive, and not ideal for the expression of idiomatic programs. The decidable Ex…
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, …
Rust combines high performance with strong memory safety through strict ownership and borrowing rules. However, its unsafe mode reintroduces vulnerabilities by allowing raw-pointer manipulation, a major source of memory-safety bugs. Existing whole-program analyses for Rust often …
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…
Coarse-Grained Reconfigurable Architectures (CGRAs) are a promising and versatile accelerator platform, offering a balance between the performance and efficiency of specialized accelerators and software programmability. However, their full potential is severely hindered by contro…
Multi-stage programming (MSP) languages such as MetaML have subtle semantics, in which familiar properties often fail to hold and hazardous interactions with other language features such as state or polymorphism abound. The ongoing incorporation of MSP features into general purpo…
Software vulnerabilities pose severe security threats, highlighting the need for effective automated detection. Directed hybrid fuzzing, which combines the rapid exploration of fuzz testing with the precise constraint solving of symbolic execution, has made notable advancements i…
Real-time systems must simultaneously deliver predictable timing, fault isolation, and memory safety, yet current operating systems expose only low-level primitives that force developers to manually balance concurrency, isolation, and performance. This paper presents LARTS, a lan…
We introduce a new two-sided type system for verifying the correctness and incorrectness of functional programs with atoms and pattern matching. A key idea in the work is that types should range over sets of normal forms, rather than sets of values, and this allows us to define a…
Global protocols specify distributed, message-passing protocols from a birds-eye view, and are used as a specification for synthesizing local implementations. Implementability asks whether a given global protocol admits a distributed implementation. We present the first comprehen…
Imprecise probability generalizes standard probability theory by replacing a single distribution with a convex set of possible distributions. We show that this generalization requires no change to the standard BDD compilation and weighted model counting pipeline used by discrete …
Relative monads provide a controlled view of computation. We generalise the monadic metalanguage to a relative setting and give a complete semantics with strong relative monads. Adopting this perspective, we generalise two existing program calculi from the literature. We provide …
Graded types provide a way to augment a type system with fine-grained information, e.g., to track side effects or context dependence and resource use (called coeffects ). Graded types for coeffects have found their way into languages such as Haskell, Idris, and Granule, enabling …
Probabilistic programming languages (PPLs) are a popular tool for high-level modelling across many fields. They provide a range of algorithms for probabilistic inference, which analyse models by learning their parameters from a dataset or estimating their posterior distributions.…
Dataflow architectures have gained renewed interest due to their balance between energy efficiency and performance. In (spatial) dataflow architectures, a program is represented as a set of entirely distributed and dynamically scheduled dataflow operators that communicate through…
Interactive Bayesian program analysis enhances static analysis by modeling derivations as probabilistic dependencies, enabling ranking alarms by calculated confidences, proposing highly likely alarms for user inspection, and updating confidences with inspection results. Existing …
In this paper, we introduce a verified framework for defining and composing sparse tensor formats. We extend the ATL tensor language and scheduling framework, which formerly could only express dense tensor kernels. We define a levelized abstraction to describe per-dimension tenso…
Agentic systems are modern software systems: they consist of orchestrated modules, expose interfaces, and are deployed in software pipelines. Unlike conventional programs, their execution, i.e., trajectories, is inherently stochastic and adaptive to the problems they are solving.…
Although reactive synthesis guarantees correct-by-construction implementations, its practical adoption is limited by a performance bottleneck in the iterative design-and-refinement cycle of formal specifications. GR(1) synthesizers perform redundant, from-scratch computations for…