35 Result(s)
within
English
Software Engineering/Programming and Operating Systems
Yi**ang Chen
Chapter
-
Chapter and Conference Paper
AISE: A Symbolic Verifier by Synergizing Abstract Interpretation and Symbolic Execution (Competition Contribution)
AISE is a static verifier that can verify the safety properties of C programs. The core of AISE is a program verification framework that synergizes abstract interpretation and symbolic execution in a novel manner...
-
Chapter and Conference Paper
FDSE: Enhance Symbolic Execution by Fuzzing-based Pre-Analysis (Competition Contribution)
FDSE serves as an automatic test generation tool designed for C programs based on symbolic execution. FDSE employs fuzzing-based pre-analysis and combines static symbolic execution and dynamic symbolic execution ...
-
Chapter and Conference Paper
Z3-Noodler: An Automata-based String Solver
Z3-Noodler is a fork of Z3 that replaces its string theory solver with a custom solver implementing the recently introduced stabilization-based algorithm for solving word equations with regular constraints. An ex...
-
Chapter and Conference Paper
Correction to: Research on Interactive Interface Design of Vehicle Warning Information Based on Context Awareness
-
Chapter and Conference Paper
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
We present a theory of Cartesian arrays, which are multi-dimensional arrays with support for the projection of arrays to sub-arrays, as well as for updating sub-arrays. The resulting logic is an extension of C...
-
Chapter and Conference Paper
AutoQ: An Automata-Based Quantum Circuit Verifier
We present a specification language and a fully automated tool named AutoQ for verifying quantum circuits symbolically. The tool implements the automata-based algorithm from [14] and extends it with the capabilit...
-
Chapter and Conference Paper
ROLL 1.0: \(\omega \) -Regular Language Learning Library
We present ROLL 1.0, an \(\omega \) -regular language learning library with command line tools to learn and ...
-
Chapter and Conference Paper
Ultimate Automizer and the Search for Perfect Interpolants
Ultimate Automizer is a software verifier that generalizes proofs for traces to proofs for larger parts for the program. In recent years the portfolio of proof producers that are available to Ultimate has grown c...
-
Chapter and Conference Paper
A Fast and Better Hybrid Recommender System Based on Spark
With the rapid development of information technology, recommender systems have become critical components to solve information overload. As an important branch, weighted hybrid recommender systems are widely u...
-
Chapter and Conference Paper
The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach
MapReduce is a popular programming model for data parallel computation. In MapReduce, the reducer produces an output from a list of inputs. Due to the scheduling policy of the platform, the inputs may arrive at t...
-
Chapter and Conference Paper
Norn: An SMT Solver for String Constraints
We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a ...
-
Chapter and Conference Paper
Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation
We apply multivariate Lagrange interpolation to synthesizing polynomial quantitative loop invariants for probabilistic programs. We reduce the computation of a quantitative loop invariant to solving constraint...
-
Chapter and Conference Paper
String Constraints for Verification
We present a decision procedure for a logic that combines (i) word equations over string variables denoting words of arbitrary lengths, together with (ii) constraints on the length of words, and on (iii) the r...
-
Chapter and Conference Paper
UKCF: A New Graphics Driver Cross-Platform Translation Framework for Virtual Machines
Virtual machine with dynamic binary translation system is the key technology to solve software compatibility problem. But traditional user space binary translation systems can’t translate hardware drivers such...
-
Chapter and Conference Paper
Reorder the Write Sequence by Virtual Write Buffer to Extend SSD’s Lifespan
The limited lifespan is the Achilles’s heel of Solid State Drive (SSD) based on NAND flash memory. NAND flash has two drawbacks that degrade SSD’s lifespan. One is the out-of-place update. Another is the seque...
-
Chapter and Conference Paper
Efficient Pipelining Parallel Methods for Image Compositing in Sort-Last Rendering
It is well known that image compositing is the bottleneck in Sort-Last rendering. Many methods have been developed to reduce the compositing time. In this paper, we present a series of pipeline methods for ima...
-
Chapter and Conference Paper
When Simulation Meets Antichains
We describe a new and more efficient algorithm for checking universality and language inclusion on nondeterministic finite word automata (NFA) and tree automata (TA). To the best of our knowledge, the antichai...
-
Chapter and Conference Paper
Study on Parallel Computing
In this talk, we present a general survey on parallel computing. The main contents include parallel computer system which is the hardware platform of parallel computing, parallel algorithm which is the theoret...
-
Chapter and Conference Paper
HAVE: Detecting Atomicity Violations via Integrated Dynamic and Static Analysis
The reality of multi-core hardware has made concurrent programs pervasive. Unfortunately, writing correct concurrent programs is difficult. Atomicity violation, which is caused by concurrently executing code u...
-
Chapter and Conference Paper
Learning Minimal Separating DFA’s for Compositional Verification
Algorithms for learning a minimal separating DFA of two disjoint regular languages have been proposed and adapted for different applications. One of the most important applications is learning minimal contextu...
