Xiaomu Shi

According to our database, Xiaomu Shi authored at least 18 papers between 2011 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking.

Li-Chang Lai, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

IACR Cryptol. ePrint Arch., 2023

llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs.

Ruiling Chen, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023

CoqCryptoLine: A Verified Model Checker with Certified Results.

Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

Certified Verification for Algebraic Abstraction.

Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU.

Vincent Hwang, Jiaxiang Liu, Gregor Seiler, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

IACR Trans. Cryptogr. Hardw. Embed. Syst., 2022

Multi-path Back-propagation Method for Neural Network Verification.

Ye Zheng, Xiaomu Shi, Jiaxiang Liu

Int. J. Softw. Informatics, 2022

Automatic Certified Verification of Cryptographic Programs with COQCRYPTOLINE.

Ming-Hsien Tsai, Yu-Fu Fu, Xiaomu Shi, Jiaxiang Liu, Bow-Yaw Wang, Bo-Yin Yang

IACR Cryptol. ePrint Arch., 2022

Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks.

Jiaxiang Liu, Yunhan Xing, Xiaomu Shi, Fu Song, Zhiwu Xu, Zhong Ming

CoRR, 2022

MpBP: verifying robustness of neural networks with multi-path bound propagation.

Ye Zheng, Jiaxiang Liu, Xiaomu Shi

Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2022

2021

CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver.

Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2019

Verifying Arithmetic in Cryptographic C Programs.

Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, 2019

Signed Cryptographic Program Verification with Typed CryptoLine.

Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2016

Safety Evaluation for Upgraded Avionics System.

Chao Zhang, Xiaomu Shi

IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2016

2015

Towards Verified Faithful Simulation.

Vania Joloboff, Jean-François Monin, Xiaomu Shi

Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2015

2013

Certification of an Instruction Set Simulator.

Xiaomu Shi

PhD thesis, 2013

Handcrafted Inversions Made Operational on Operational Semantics.

Jean-François Monin, Xiaomu Shi

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

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

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

Proceedings of the Certified Programs and Proofs - First International Conference, 2011