Skip to main content

and
  1. No Access

    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 \) ...

    Yong Li, Andrea Turrini, Yu-Fang Chen in Engineering Trustworthy Software Systems (2019)

  2. No Access

    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...

    Yuanrui Zhang, Hengyang Wu, Yixiang Chen in Formal Techniques for Safety-Critical Syst… (2019)

  3. No Access

    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...

    Yang Chen, Zhenya Zhang, Peng Wu, Yu Zhang in Dependable Software Engineering. Theories,… (2018)

  4. 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...

    Yong Li, Yu-Fang Chen, Lijun Zhang in Tools and Algorithms for the Construction … (2017)

  5. 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...

    Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai in Tools and Algorithms for the Construction … (2015)

  6. 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...

    Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha in Tools and Algorithms for the Construction … (2015)

  7. No Access

    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 ...

    Paul C. Bell, Shang Chen in Reachability Problems (2013)

  8. No Access

    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...

    Chengsong Wang, Zhenbang Chen, **aoguang Mao in Runtime Verification (2013)