Xiaomu Shi

ORCID

Publication Activity (10 Years)

Years Active: 2011-2024
Publications (10 Years): 14

Top Venues

IACR Cryptol. ePrint Arch.

CAV (2)

ESEC/SIGSOFT FSE

IACR Trans. Cryptogr. Hardw. Embed. Syst.

University of Grenoble, France (PHD)

Education History

University of Grenoble, France

PHD

Publications

Jiaxiang Liu, Yunhan Xing, Xiaomu Shi, Fu Song, Zhiwu Xu, Zhong Ming
Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks. ACM Trans. Softw. Eng. Methodol. 33 (5) (2024)
Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang
Certified Verification for Algebraic Abstraction. CAV (3) (2023)
Ruiling Chen, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs. ESEC/SIGSOFT FSE (2023)
Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking. IACR Cryptol. ePrint Arch. 2023 (2023)
Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang
CoqCryptoLine: A Verified Model Checker with Certified Results. CAV (2) (2023)
Vincent Hwang, Jiaxiang Liu, Gregor Seiler, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2022 (4) (2022)
Jiaxiang Liu, Yunhan Xing, Xiaomu Shi, Fu Song, Zhiwu Xu, Zhong Ming
Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks. CoRR (2022)
Ye Zheng, Jiaxiang Liu, Xiaomu Shi
MpBP: verifying robustness of neural networks with multi-path bound propagation. ESEC/SIGSOFT FSE (2022)
Ye Zheng, Xiaomu Shi, Jiaxiang Liu
Multi-path Back-propagation Method for Neural Network Verification. Int. J. Softw. Informatics 12 (4) (2022)
Ming-Hsien Tsai, Yu-Fu Fu, Xiaomu Shi, Jiaxiang Liu, Bow-Yaw Wang, Bo-Yin Yang
Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE. IACR Cryptol. ePrint Arch. 2022 (2022)
Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. CAV (2) (2021)
Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Signed Cryptographic Program Verification with Typed CryptoLine. CCS (2019)
Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Verifying Arithmetic in Cryptographic C Programs. ASE (2019)
Chao Zhang, Xiaomu Shi
Safety Evaluation for Upgraded Avionics System. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. (4) (2016)
Vania Joloboff, Jean-François Monin, Xiaomu Shi
Towards Verified Faithful Simulation. SETTA (2015)
Jean-François Monin, Xiaomu Shi
Handcrafted Inversions Made Operational on Operational Semantics. ITP (2013)
Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui
First steps towards the certification of an ARM simulator using Compcert CoRR (2012)
Frédéric Blanqui, Claude Helmstetter, Vania Joloboff, Jean-François Monin, Xiaomu Shi
Designing a CPU model: from a pseudo-formal document to fast code CoRR (2011)
Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui
First Steps towards the Certification of an ARM Simulator Using Compcert. CPP (2011)

Xiaomu Shi.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Xiaomu Shi