First Steps towards the Certification of an ARM Simulator Using Compcert. - Xiaomu Shi; Jean-François Monin; Frédéric Tuong; Frédéric Blanqui (CPP, 2011)

Designing a CPU model: from a pseudo-formal document to fast code - Frédéric Blanqui; Claude Helmstetter; Vania Joloboff; Jean-François Monin; Xiaomu Shi (CoRR, 2011)

Handcrafted Inversions Made Operational on Operational Semantics. - Jean-François Monin; Xiaomu Shi (ITP, 2013)

Certification of an Instruction Set Simulator. - Xiaomu Shi (2013)

Towards Verified Faithful Simulation. - Vania Joloboff; Jean-François Monin; Xiaomu Shi (SETTA, 2015)

Safety Evaluation for Upgraded Avionics System. - Chao Zhang; Xiaomu Shi (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2016)

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)

Verifying Arithmetic in Cryptographic C Programs. - Jiaxiang Liu 001; Xiaomu Shi; Ming-Hsien Tsai 001; Bow-Yaw Wang; Bo-Yin Yang (ASE, 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)

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)

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)

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)

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)