26,098 papers · page 158 of 1,305
Abstract In this paper, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans, including arithmetic theories. Our approach transforms theory specifications into purely Boolean specifications by (1) substituting theory literals b…
Abstract The simulation of quantum circuits on classical computers is an important problem in quantum computing. Such simulation requires representations of distributions over very large sets of basis vectors, and recent work has used symbolic data-structures such as Binary Decis…
Abstract Identifying live and dead states in an abstract transition system is a recurring problem in formal verification; for example, it arises in our recent work on efficiently deciding regex constraints in SMT. However, state-of-the-art graph algorithms for maintaining reachab…
Abstract Probabilistic recurrence relations (PRRs) are a standard formalism for describing the runtime of a randomized algorithm. Given a PRR and a time limit $$\kappa $$ κ , we consider the tail probability $$\Pr [T \ge \kappa ]$$ Pr [ T ≥ κ ] , i.e., the probability that the ra…
Abstract Logic locking was designed to be a formidable barrier to IP piracy: given a logic design, logic locking modifies the logic design such that the circuit operates correctly only if operated with the “correct”secretkey. However, strong attacks (like SAT-based attacks) soon …
Abstract We present a certified algebraic abstraction technique for verifying bit-accurate non-linear integer computations. In algebraic abstraction, programs are lifted to polynomial equations in the abstract domain. Algebraic techniques are employed to analyze abstract polynomi…
Abstract We present the verified model checker CoqCryptoLine for cryptographic programs with certified verification results. The CoqCryptoLine verification algorithm consists of two reductions. The algebraic reduction transforms into a root entailment problem; and the bit-vector …
Abstract We present a major new version of Scenic, a probabilistic programming language for writing formal models of the environments of cyber-physical systems. Scenic has been successfully used for the design and analysis of CPS in a variety of domains, but earlier versions are …
Abstract This paper proposes an automated method to check the correctness of range analysis used in the Linux kernel ’s eBPF verifier. We provide the specification of soundness for range analysis performed by the eBPF verifier. We automatically generate verification conditions th…
Abstract We present an algorithm to learn a deterministic timed automaton (DTA) via membership and equivalence queries. Our algorithm is an extension of the L* algorithm with a Myhill-Nerode style characterization of recognizable timed languages, which is the class of timed langu…
Abstract We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language ofstring diagrams. The algorithm computes optimal expected rewards. Our theoretical development of the algorithm is support…
Abstract Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leav…
Abstract / and its variants have been the prominent approaches to safety model checking in recent years. Compared to the previous model-checking algorithms like (Bounded Model Checking) and (Interpolation Model Checking), / is attractive due to its completeness (vs. ) and scalabi…
Abstract The problem of model counting, also known as $$\#\textsf{SAT}$$ , is to compute the number of models or satisfying assignments of a given Boolean formula F. Model counting is a fundamental problem in computer science with a wide range of applications. In recent years, th…
Abstract There is a pressing need for learning controllers to endow systems with properties of safety and goal-reaching, which are crucial for many safety-critical systems. Reinforcement learning (RL) has been deployed successfully to synthesize controllers from user-defined rewa…
Abstract Online monitoring is an effective validation approach for hybrid systems, that, at runtime, checks whether the (partial) signals of a system satisfy a specification in, e.g., Signal Temporal Logic (STL) . The classic STL monitoring is performed by computing a robustness …
Abstract Dubbed a safer C, Rust is a modern programming language that combines memory safety and low-level control. This interesting combination has made Rust very popular among developers and there is a growing trend of migrating legacy codebases (very often in C) to Rust. In th…
Abstract To alleviate the practical constraints for deploying deep neural networks (DNNs) on edge devices, quantization is widely regarded as one promising technique. It reduces the resource requirements for computational power and storage space by quantizing the weights and/or a…
The Java Vector API is a new module introduced in Java 16, allowing developers to concisely express vector computations. The API promises both high performance, achieved via the runtime compilation of vector operations to hardware vector instructions, and portability. To the best…
We present an adaptation to the LLVM greedy register allocator to improve code density for compressed RISC ISAs. Many RISC architectures have extensions defining smaller encodings for common instructions, typically 16 rather than 32 bits wide. However, these instructions typical…