7,482 papers · page 16 of 375
This work introduces StageSAT , a new approach to solving floating-point satisfiability that bridges SMT solving with numerical optimization. StageSAT reframes a floating-point formula as a series of optimization problems in three stages, each with increasing precision. It begins…
Modern processors integrate heterogeneous devices to expose unified shared memory. Yet, the de-facto design pattern used to compose their disparate coherence protocols lacks a formal foundation. This leaves the door open for subtle consistency bugs, in a critical gap between prac…
The design of scientific experiments deserves its own variation of formal verification to catch cases where scientists made important mistakes, such as forgetting to take confounding variables into account. One of the most fundamental underpinnings of science is causality , or wh…
Deep learning (DL) libraries are widely used in critical applications, where even subtle silent bugs can lead to serious consequences. While existing DL fuzzing techniques have made progress in detecting crashes, they inherently struggle to detect silent bugs due to the lack of e…
We propose a novel approach that leverages Bayesian program analysis to guide large-scale target-guided greybox fuzzing (LTGF). LTGF prioritizes program locations (targets) that are likely to contain bugs and applies directed mutation towards high-priority targets. However, exist…
Operator fusion has become a key optimization for deep learning, which combines multiple deep learning operators to improve data reuse and reduce global memory transfers. However, existing tensor compilers struggle to fuse complex reduction computations involving loop-carried dep…
Several recently proposed program logics have incorporated notions of under approximation into their design, enabling them to reason about reachability rather than safety. In this paper, we explore how similar ideas can be integrated into an expressive type and effect system. We …
We propose a method for mechanically translating iterative dataflow analysis (IDA) algorithms to algebraic program analysis (APA) algorithms capable of computing exactly the same set of dataflow facts. The method is useful because while most of the dataflow analysis algorithms us…
Binary lifting, which translates binary code into LLVM intermediate representations (IRs) through iterative IR transformations for recovering high-level constructs from low-level machine features, is the cornerstone of many binary analysis systems. Therefore, the scalability and …
Weak monadic second-order logic ( wMSO ) is a foundational tool for specifying regular properties. Traditional decision procedures for this logic typically translate wMSO formulas into finite automata. Although the logic is decidable, this approach incurs non-elementary complexit…
GPUs play an increasingly important role in modern software. However, the heterogeneous host-device execution model and expanding software stacks make GPU programs prone to memory-safety and concurrency bugs that evade static analysis. While fuzz-testing, combined with dynamic er…
Backward stability is a desirable property for a well-designed numerical algorithm: given an input, a backward stable floating-point program produces the exact output for a nearby input. While automated tools for bounding the forward error of a numerical program are well-establis…
Although randomization has long been used in distributed computing, formal methods for reasoning about probabilistic concurrent programs have lagged behind. No existing program logics can express specifications about the full distributions of outcomes resulting from programs that…
Recent research has demonstrated the effectiveness of extending the Hindley-Milner (HM) type system with Boolean kinds to support type inference for a wide variety of features. However, the means to support classic type system provisions such as local let generalization and polym…
Compared to familiar hardware-description languages like Verilog, rule-based languages like Bluespec offer opportunities to import modularity features from software programming. While Verilog modules are about connecting wires between submodules, Bluespec modules resemble objects…
Data processing frameworks like Apache Spark and Flink provide built-in support for user-defined aggregation functions (UDAFs), enabling the integration of domain-specific logic. However, for these frameworks to support efficient UDAF execution, the function needs to satisfy a ho…
Virtual memory management (VMM) code is a critical piece of general-purpose OS kernels, but verification of this functionality is challenging due to the complexity of the hardware interface (the page tables are updated via writes to those memory locations, using addresses which a…
Proof assistants based on type theories have been widely successful from verifying safety-critical software to establishing a new standard of rigour by formalizing mathematics. But these proof assistants and even their type-checking kernels are also complex pieces of software, an…
Local reasoning about programs that combine aliasing and mutable state is a longstanding challenge. Existing approaches – ownership systems, linear and affine types, uniqueness types, and lexical effect tracking – impose global restrictions such as uniqueness or linearity, or rel…
Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is compositionali…