From diagrammatic confluence to modularity. - Jean-Pierre Jouannaud; Jiaxiang Liu 001 (Theor. Comput. Sci., 2012)

Confluence: The Unifying, Expressive Power of Locality. - Jiaxiang Liu 001; Jean-Pierre Jouannaud (Specification, Algebra, and Software, 2014)

Confluence by Critical Pair Analysis. - Jiaxiang Liu 001; Nachum Dershowitz; Jean-Pierre Jouannaud (RTA-TLCA, 2014)

Confluence of Layered Rewrite Systems. - Jiaxiang Liu 001; Jean-Pierre Jouannaud; Mizuhito Ogawa (CSL, 2015)

Confluence properties of rewrite rules by decreasing diagrams. (Propriétés de confluence des règles de réécriture par des diagrammes décroissants). - Jiaxiang Liu 001 (2016)

Formal Modeling and Verification of a Rate-Monotonic Scheduling Implementation with Real-Time Maude. - Jiaxiang Liu 001; Min Zhou 001; Xiaoyu Song; Ming Gu 001; Jiaguang Sun 001 (IEEE Trans. Ind. Electron., 2017)

Signed Cryptographic Program Verification with Typed CryptoLine. - Yu-Fu Fu; Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CCS, 2019)

An Empirical Study on API-Misuse Bugs in Open-Source C Programs. - Zuxing Gu; Jiecheng Wu; Jiaxiang Liu 001; Min Zhou 001; Ming Gu 001 (COMPSAC (1), 2019)

Verifying Arithmetic in Cryptographic C Programs. - Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (ASE, 2019)

IMSpec: An Extensible Approach to Exploring the Incorrect Usage of APIs. - Zuxing Gu; Min Zhou 001; Jiecheng Wu; Yu Jiang 001; Jiaxiang Liu 001; Ming Gu 001 (TASE, 2019)

CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. - Xiaomu Shi; Yu-Fu Fu; Jiaxiang Liu 001; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (CAV (2), 2021)

CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial Attacks. - Zhe Zhao 007; Yedi Zhang; Guangke Chen; Fu Song; Taolue Chen 001; Jiaxiang Liu 001 (SAS, 2022)

MpBP: verifying robustness of neural networks with multi-path bound propagation. - Ye Zheng; Jiaxiang Liu 001; Xiaomu Shi (ESEC/SIGSOFT FSE, 2022)

Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE. - Ming-Hsien Tsai 001; Yu-Fu Fu; Xiaomu Shi; Jiaxiang Liu 001; Bow-Yaw Wang; Bo-Yin Yang (IACR Cryptol. ePrint Arch., 2022)

Multi-path Back-propagation Method for Neural Network Verification. - Ye Zheng; Xiaomu Shi; Jiaxiang Liu 001 (Int. J. Softw. Informatics, 2022)

Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU. - Vincent Hwang; Jiaxiang Liu 001; Gregor Seiler; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2022)

Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. - Gilles Dowek; Gaspard Férey; Jean-Pierre Jouannaud; Jiaxiang Liu 001 (Math. Struct. Comput. Sci., 2022)

Certified Verification for Algebraic Abstraction. - Ming-Hsien Tsai 001; Yu-Fu Fu; Jiaxiang Liu 001; Xiaomu Shi; Bow-Yaw Wang; Bo-Yin Yang (CAV (3), 2023)

CoqCryptoLine: A Verified Model Checker with Certified Results. - Ming-Hsien Tsai 001; Yu-Fu Fu; Jiaxiang Liu 001; Xiaomu Shi; Bow-Yaw Wang; Bo-Yin Yang (CAV (2), 2023)

Boosting Multi-neuron Convex Relaxation for Neural Network Verification. - Xuezhou Tang; Ye Zheng; Jiaxiang Liu 001 (SAS, 2023)

llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs. - Ruiling Chen; Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (ESEC/SIGSOFT FSE, 2023)

Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking. - Li-Chang Lai; Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (IACR Cryptol. ePrint Arch., 2023)

Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once. - Weizhi Feng; Yicheng Liu; Jiaxiang Liu 001; David N. Jansen; Lijun Zhang 001; Zhilin Wu (DAC, 2024)

Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks. - Jiaxiang Liu 001; Yunhan Xing; Xiaomu Shi; Fu Song; Zhiwu Xu 001; Zhong Ming 001 (ACM Trans. Softw. Eng. Methodol., 2024)

Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography. - Chun-Ming Chiu; Jiaxiang Liu 001; Ming-Hsien Tsai 001; Xiaomu Shi; Bow-Yaw Wang; Bo-Yin Yang (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2025)