15 Result(s)
within
English
Computer Science
Algorithm Analysis and Problem Complexity
Logics and Meanings of Programs
Software Engineering
Yi**ang Chen
Chapter
-
Chapter
Learning Büchi Automata and Its Applications
In this work, we review an algorithm that learns a Büchi automaton from a teacher who knows an \(\omega \) ...
-
Chapter and Conference Paper
Embedding CCSL into Dynamic Logic: A Logical Approach for the Verification of CCSL Specifications
The Clock Constraint Specification Language (CCSL) is a clock-based specification language for capturing causal and chronometric constraints between events in Real-Time Embedded Systems (RTESs). Due to the lim...
-
Chapter and Conference Paper
Interleaving-Tree Based Fine-Grained Linearizability Fault Localization
Linearizability is an important correctness criterion for concurrent objects. Existing work mainly focuses on linearizability verification of coarse-grained traces with operation invocations and responses only...
-
Chapter and Conference Paper
An Executable Sequential Specification for Spark Aggregation
Spark is a new promising platform for scalable data-parallel computation. It provides several high-level application programming interfaces (APIs) to perform parallel data aggregation. Since execution of paral...
-
Chapter and Conference Paper
A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees
In this paper, we propose a novel algorithm to learn a Büchi automaton from a teacher who knows an \(\omega \) -regula...
-
Chapter and Conference Paper
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation
CPArec is a tool for verifying recursive C programs via source-to-source program transformation. It uses a recursion-free program analyzer CPAChecker as a black box and computes function summar...
-
Chapter and Conference Paper
Commutativity of Reducers
In the Map-Reduce programming model for data parallel computation, a reducer computes an output from a list of input values associated with a key. The inputs however may not arrive at a reducer in a fixed orde...
-
Chapter and Conference Paper
BULL: A Library for Learning Algorithms of Boolean Functions
We present the tool BULL (Boolean fUnction Learning Library), the first publicly available implementation of learning algorithms for Boolean functions. The tool is implemented in C with interfaces to C++, JAVA...
-
Chapter and Conference Paper
Reachability Problems for Hierarchical Piecewise Constant Derivative Systems
In this paper, we investigate the computability and complexity of reachability problems for two-dimensional hierarchical piecewise constant derivative (HPCD) systems. The main interest in HPCDs stems from the ...
-
Chapter and Conference Paper
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO
We introduce Memorax, a tool for the verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range and integer variables and running on top of weak memory m...
-
Chapter and Conference Paper
Optimizing Nop-shadows Typestate Analysis by Filtering Interferential Configurations
Nop-shadows Analysis (NSA) is an efficient static typestate analysis, which can be used to eliminate unnecessary monitoring instrumentations for runtime monitors. In this paper, we propose two optimizations to...
-
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...
-
Chapter and Conference Paper
GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
This paper reports extensions to the GOAL tool that enable it to become a research tool for omega automata and temporal logic. The extensions include an expanded collection of translation, simplification, and ...
-
Chapter and Conference Paper
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
Recent studies have suggested the applicability of learning to automated compositional verification. However, current learning algorithms fall short when it comes to learning liveness properties. We extend the au...
-
Chapter and Conference Paper
GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae
In this paper, we present a tool named GOAL (an acronym derived from “Graphical Tool for Omega-Automata and Logics”) whose main functions include (1) drawing and testing Büchi automata, (2) checking the language ...
