Xiaomu Shi

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