Traceability and model checking to support safety requirement verification. - Shuanglong Kan (SIGSOFT FSE, 2014)

Partial Order Reduction for State/Event Systems. - Shuanglong Kan; Zhiqiu Huang; Zhe Chen 011 (ICFEM, 2016)

面向DO-333的襟缝翼控制单元安全性分析 (Safety Analysis of Slat and Flap Control Unit for DO-333). - Guangying Chen; Zhiqiu Huang; Zhe Chen 011; Shuanglong Kan (计算机科学, 2016)

A refinement-based compiler development for synchronous languages. - Jean-Paul Bodeveix; Mamoun Filali-Amine; Shuanglong Kan (MEMOCODE, 2017)

A Better Translation From LTL to Transition-Based Generalized Büchi Automata. - Weiwei Li 001; Shuanglong Kan; Zhiqiu Huang (IEEE Access, 2017)

Partial order reduction for checking LTL formulae with the next-time operator. - Shuanglong Kan; Zhiqiu Huang; Zhe Chen 011; Weiwei Li 001; Yutao Huang (J. Log. Comput., 2017)

Partial Order Reduction for the full Class of State/Event Linear Temporal Logic. - Shuanglong Kan; Zhiqiu Huang (Comput. J., 2018)

Executable Operational Semantics of Solidity. - Jiao Jiao 002; Shuanglong Kan; Shang-Wei Lin 001; David Sanán; Yang Liu 003; Jun Sun 001 (CoRR, 2018)

K-Rust: An Executable Formal Semantics for Rust. - Shuanglong Kan; David Sanán; Shang-Wei Lin 001; Yang Liu 003 (CoRR, 2018)

Detecting safety-related components in statecharts through traceability and model slicing. - Shuanglong Kan; Zhiqiu Huang (Softw. Pract. Exp., 2018)

A Formally Verified Buddy Memory Allocation Model. - Ke Jiang; David Sanán; Yongwang Zhao; Shuanglong Kan; Yang Liu 003 (ICECCS, 2019)

Detecting memory errors at runtime with source-level instrumentation. - Zhe Chen 011; Junqi Yan; Shuanglong Kan; Ju Qian; Jingling Xue (ISSTA, 2019)

Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity. - Jiao Jiao 002; Shuanglong Kan; Shang-Wei Lin 001; David Sanán; Yang Liu 003; Jun Sun 001 (SP, 2020)

A security type verifier for smart contracts. - Xinwen Hu; Yi Zhuang 002; Shangwei Lin 001; Fuyuan Zhang; Shuanglong Kan; Zining Cao (Comput. Secur., 2021)

CertiStr: A Certified String Solver (technical report). - Shuanglong Kan; Anthony W. Lin; Philipp Rümmer; Micha Schrader (CoRR, 2021)

CertiStr: a certified string solver. - Shuanglong Kan; Anthony Widjaja Lin; Philipp Rümmer; Micha Schrader (CPP, 2022)

Solving string constraints with Regex-dependent functions through transducers with priorities and variables. - Taolue Chen 001; Alejandro Flores-Lamas; Matthew Hague; Zhilei Han; Denghang Hu; Shuanglong Kan; Anthony W. Lin; Philipp Rümmer; Zhilin Wu (Proc. ACM Program. Lang., 2022)

SafeOSL: Ensuring memory safety of C via ownership-based intermediate language. - Xiaohua Yin; Zhiqiu Huang; Shuanglong Kan; Guohua Shen; Zhe Chen 011; Yang Liu 003; Fei Wang 032 (Softw. Pract. Exp., 2022)

Formally understanding Rust's ownership and borrowing system at the memory level. - Shuanglong Kan; Zhe Chen 011; David Sanán; Yang Liu 003 (Formal Methods Syst. Des., 2024)

Certified Symbolic Transducer with Applications in String Solving. - Shuanglong Kan (CoRR, 2025)