Model Checking & Markov Decision Process
Formal Derivation and Verification of Critical Path Algorithm for Directed Acyclic Graph
An Approach of Transforming Non-Markovian Reward to Markovian Reward
A JPSL based Model Checking Approach for Java Programs
Model Analysis & Tool Implementation
Implementation of Matlab matfun Toolkit Based on MSVL
Extending Visibly Pushdown Automata over Multi-matching Nested Relations
Schedulability analysis of rate-monotonic algorithm on concurrent execution of digraph real-time tasks
Formal Specification & Testing
Formalization of natural language into PPTL specification via neural machine translation
Testing Program Segments to Detect Runtime Exceptions in Java
Inferring Exact Domains to Efficiently Generate Valid Test Cases via Testing
Algorithms & Verification
Testing and Verifying the security of COVID-19 CT Images Deep Learning System with Adversarial Attack
Verifying and improving neural networks using testing-based formal verification
Alternating Projection Temporal Epistemic Logic.