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.