26,098 papers · page 38 of 1,305
Abstract Bespoke data structure operations are common in real-world C code. We identify one common subclass, monotonic data structure traversals (MDSTs), that iterate monotonically through the structure. For example, iterates from start to end of a character array until a null by…
Abstract We introduce $$(\varepsilon, \delta)$$ ( ε , δ ) -bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $$(\varepsilon, \delta)$$ ( ε , δ ) -bisimulation allows the use of different toleran…
Abstract Circuit languages like Circom and Gnark have become essential tools for programmable zero-knowledge cryptography, allowing developers to build privacy-preserving applications. These domain-specific languages (DSLs) encode both the computation to be verified (as a witness…
Abstract In this paper, we present rIC3, an efficient bit-level hardware model checker primarily based on the IC3 algorithm. It boasts a highly efficient implementation and integrates several recently proposed optimizations, such as the specifically optimized SAT solver, dynamica…
Abstract The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and completeness. It utilizes SAT solvers to solve a series of SAT queries associated with relati…
Abstract Neural networks are often susceptible to minor perturbations in input that cause them to misclassify. A recent solution to this problem is the use of globally-robust neural networks, which employ a function to certify that the classification of an input cannot be altered…
Abstract This paper presents StarV, a new tool for verifying deep neural networks (DNNs) and learning-enabled Cyber-Physical Systems (Le-CPS) using the well-known star reachability. Distinguished from existing star-based verification tools such as NNV and NNENUM and others, StarV…
Abstract We develop decision procedures for extended regular expressions in the new $$\textbf{ERE} \texttt {\#}$$ ERE # framework that uses span semantics , utilizing the power of symbolic derivatives . We prove a normal form theorem in Lean for $$\textbf{ERE} \texttt {\#}$$ ERE …
Abstract Applications of decision diagrams in quantum circuit analysis have been an active research area. Our work introduces FeynmanDD, a new method utilizing standard and multi-terminal decision diagrams for quantum circuit simulation and equivalence checking. Unlike previous a…
Abstract We propose a deductive synthesis framework for constructing reinforcement learning (RL) agents that provably satisfy temporal reach-avoid specifications over infinite horizons. Our approach decomposes these temporal specifications into a sequence of finite-horizon subtas…
Abstract Deep Neural Networks (DNN) are crucial in approximating nonlinear functions across diverse applications, ranging from image classification to control. Verifying specific input-output properties can be a highly challenging task due to the lack of a single, self-contained …
Abstract Automatically constructing smooth paths that satisfy a formal specification is a challenging problem. Existing methods struggle to scale to long horizon specifications and challenging environments. We present a method that uses abstraction, model checking, and convex opt…
Abstract Memory safety is a fundamental correctness property of software. For programs that manipulate linked, heap-allocated data structures, ensuring memory safety requires analyzing their possible shapes. Despite significant advances in shape analysis, existing techniques rely…
Abstract Labelled Dirac notation is a formalism commonly used by physicists to represent many-body quantum systems and by computer scientists to assert properties of quantum programs. It is supported by a rich equational theory for proving equality between expressions in the lang…
Abstract Floating-point accumulation networks (FPANs) are key building blocks used in many floating-point algorithms, including compensated summation and double-double arithmetic. FPANs are notoriously difficult to analyze, and algorithms using FPANs are often published without r…
Data flow analysis is fundamental to modern program optimization and verification, serving as a critical foundation for compiler transformations. As machine learning increasingly drives compiler tasks, the need for models that can implicitly understand and correctly reason about …
Tensor compilers like XLA, TVM, and TensorRT operate on computational graphs, where vertices represent operations and edges represent data flow between these operations. Operator fusion is an optimization that merges operators to improve their efficiency. This paper presents the …
Research on novel Instruction Set Architectures (ISAs) is actively pursued; however, it requires extensive efforts to develop and maintain comprehensive compilation toolchains for each new ISA. Binary translation can provide a practical solution for ISA researchers to port target…
Random test case generation is a challenging subject in compiler testing. Due to the structured and strict nature of the languages required for compiler inputs, using randomization techniques for hunting bugs in compiler implementation represents a big challenge that requires tra…
Large Language Models (LLMs) have demonstrated remarkable capabilities across a variety of software engineering and coding tasks. However, their application in the domain of code and compiler optimization remains underexplored. Training LLMs is resource-intensive, requiring subst…