Graphs and Graph Transformations for Object-Oriented and Service-Oriented Systems. - Liang Zhao 021 (2012)

Graph-Based Object-Oriented Hoare Logic. - Liang Zhao 021; Shuling Wang; Zhiming Liu 001 (Theories of Programming and Formal Methods, 2013)

An Interface Model of Software Components. - Ruzhen Dong; Naijun Zhan; Liang Zhao 021 (ICTAC, 2013)

Formalizing and Implementing Types in MSVL. - Xiaobing Wang; Zhenhua Duan; Liang Zhao 021 (SOFL+MSVL, 2013)

A sound and complete theory of graph transformations for service programming with sessions and pipelines. - Liang Zhao 021; Roberto Bruni 001; Zhiming Liu 001 (Sci. Comput. Program., 2014)

Runtime Verification Monitor Construction for Three-valued PPTL. - Xiaobing Wang; Dongmiao Liu; Liang Zhao 021; Yina Xue (SOFL+MSVL, 2016)

A Framework Based on MSVL for Verifying Probabilistic Properties in Social Networks. - Xiaobing Wang; Liyuan Ren; Liang Zhao 021; Xinfeng Shu (SOFL+MSVL, 2017)

MSVL: a typed language for temporal logic programming. - Xiaobing Wang; Cong Tian; Zhenhua Duan; Liang Zhao 021 (Frontiers Comput. Sci., 2017)

Reducing Extension Edges of Concurrent Programs for Reachability Analysis. - Cong Tian; Jiaying Wang; Zhenhua Duan; Liang Zhao 021 (COCOA, 2018)

RFC-directed differential testing of certificate validation in SSL/TLS implementations. - Chu Chen; Cong Tian; Zhenhua Duan; Liang Zhao 021 (ICSE, 2018)

Model Checking Java Programs with MSVL. - Xinfeng Shu; Na Luo; Bo Wang; Xiaobing Wang; Liang Zhao 021 (SOFL+MSVL, 2018)

Runtime Verification Method for Social Network Security Based on Source Code Instrumentation. - Xiaobing Wang; Wenxuan Guo; Liang Zhao 021; Xinfeng Shu (SOFL+MSVL, 2018)

A Proof System for a Unified Temporal Logic. - Liang Zhao 021; Xiaobing Wang; Xinfeng Shu; Nan Zhang 001 (COCOON, 2019)

Model Checking Python Programs with MSVL. - Xinfeng Shu; Fengyun Gao; Weiran Gao; Lili Zhang; Xiaobing Wang; Liang Zhao 021 (SOFL+MSVL, 2019)

Towards Formal Verification of Neural Networks: A Temporal Logic Based Framework. - Xiaobing Wang; Kun Yang; Yanmei Wang; Liang Zhao 021; Xinfeng Shu (SOFL+MSVL, 2019)

Model checking of pushdown systems for projection temporal logic. - Liang Zhao 021; Xiaobing Wang; Zhenhua Duan (Theor. Comput. Sci., 2019)

Differential Testing of Certificate Validation in SSL/TLS Implementations: An RFC-guided Approach. - Cong Tian; Chu Chen; Zhenhua Duan; Liang Zhao 021 (ACM Trans. Softw. Eng. Methodol., 2019)

An MSVL Based Model Checking Method for Multi-threaded C Programs. - Xinfeng Shu; Zhenyu Wang; Weiran Gao; Xiaobing Wang; Liang Zhao 021 (SOFL+MSVL, 2020)

Automatic Generation of Specification from Natural Language Based on Temporal Logic. - Xiaobing Wang; Ge Li; Chunyi Li; Liang Zhao 021; Xinfeng Shu (SOFL+MSVL, 2020)

An MSVL-Based Modeling Framework for Back Propagation Neural Networks. - Liang Zhao 021; Zhe Feng; Xiaobing Wang; Xinfeng Shu (SOFL+MSVL, 2020)

Efficient decision procedure for propositional projection temporal logic. - Xinfeng Shu; Nan Zhang 001; Xiaobing Wang; Liang Zhao 021 (Theor. Comput. Sci., 2020)

A sound and complete proof system for a unified temporal logic. - Liang Zhao 021; Xiaobing Wang; Xinfeng Shu; Nan Zhang 001 (Theor. Comput. Sci., 2020)

RTPDroid: Detecting Implicitly Malicious Behaviors Under Runtime Permission Model. - Jie Zhang 084; Cong Tian; Zhenhua Duan; Liang Zhao 021 (IEEE Trans. Reliab., 2021)

Formal Modeling and Verification of Convolutional Neural Networks based on MSVL. - Liang Zhao 021; Leping Wu; Yu Gao; Xiaobing Wang; Bin Yu 008 (DSA, 2022)

Driver Violation Prediction based on Neural Network. - Xingguang Zhu; Jiajun Chang; Weikang Li; Bin Yu 008; Liang Zhao 021; Xiaobing Wang (DSA, 2022)

Formalization of Natural Language into PPTL Specification via Neural Machine Translation. - Chunyi Li; Jiajun Chang; Xiaobing Wang; Liang Zhao 021; Wenjie Mao (SOFL+MSVL, 2022)

Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-Triggering. - Bin Yu 008; Cong Tian; Hengrui Xing; Zuchao Yang; Jie Su 002; Xu Lu 003; Jiyu Yang; Liang Zhao 021; Xiaofeng Li; Zhenhua Duan (ESEC/SIGSOFT FSE, 2023)

Efficient verification of neural networks based on neuron branching and LP abstraction. - Liang Zhao 021; Xinmin Duan; Chenglong Yang; Yuehao Liu; Yansong Dong; Xiaobing Wang; Wensheng Wang (Neurocomputing, 2024)

Multi-keyword ranked search with access control for multiple data owners in the cloud. - Jiaqi Guo; Cong Tian; Xu Lu 003; Liang Zhao 021; Zhenhua Duan (J. Inf. Secur. Appl., 2024)

Verifiable privacy-preserving semantic retrieval scheme in the edge computing. - Jiaqi Guo; Cong Tian; Qiang He; Liang Zhao 021; Zhenhua Duan (J. Syst. Archit., 2024)

Neuron importance based verification of neural networks via divide and conquer. - Yansong Dong; Yuehao Liu; Liang Zhao 021; Cong Tian; Zhenhua Duan (Neurocomputing, 2024)

A multi-granularity CNN pruning framework via deformable soft mask with joint training. - Peng Zhang; Cong Tian; Liang Zhao 021; Zhenhua Duan (Neurocomputing, 2024)

Requirement specification extraction and analysis based on propositional projection temporal logic. - Xiaobing Wang; Chunyi Li; Liang Zhao 021 (J. Softw. Evol. Process., 2024)

Intra-head pruning for vision transformers via inter-layer dimension relationship modeling. - Peng Zhang; Cong Tian; Liang Zhao 021; Zhenhua Duan (Neural Networks, 2025)

AutoTestForge: A Multidimensional Automated Testing Framework for Natural Language Processing Models. - Hengrui Xing; Cong Tian; Liang Zhao 021; Zhi Ma; Wensheng Wang; Nan Zhang 001; Chao Huang; Zhenhua Duan (CoRR, 2025)