Demystifying Template-Based Invariant Generation for Bit-Vector Programs. - Peisen Yao; Jingyu Ke; Jiahui Sun; Hongfei Fu 001; Rongxin Wu; Kui Ren 001 (ASE, 2023)

Affine Disjunctive Invariant Generation with Farkas' Lemma. - Hongming Liu; Jingyu Ke; Hongfei Fu 001; Liqian Chen; Guoqiang Li 001 (CoRR, 2023)

Piecewise Linear Expectation Analysis via k-Induction for Probabilistic Programs. - Tengshun Yang; Hongfei Fu 001; Jingyu Ke; Naijun Zhan; Shiyang Wu (CoRR, 2024)

Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models. - Ruibang Liu; Guoqiang Li 001; Minyu Chen; Ling-I Wu; Jingyu Ke (CoRR, 2024)

Push-Button Verification for BitVM Implementations. - Hanzhi Liu; Jingyu Ke; Hongbo Wen; Robin Linus; Lukas George; Manish Bista; Hakan Karakus; Domo; Junrui Liu; Yanju Chen; Yu Feng 001 (IACR Cryptol. ePrint Arch., 2024)

Affine Disjunctive Invariant Generation with Farkas' Lemma. - Jingyu Ke; Hongfei Fu 001; Hongming Liu; Zhouyue Sun; Liqian Chen; Guoqiang Li 001 (VMCAI (1), 2025)

ZK-ProVer: Proving Programming Verification in Non-Interactive Zero-Knowledge Proofs. - Haoyu Wei; Jingyu Ke; Ruibang Liu; Guoqiang Li (IACR Cryptol. ePrint Arch., 2025)

Thunderbolt: A Formally Verified Protocol for Off-Chain Bitcoin Transfers. - Hongbo Wen; Hanzhi Liu; Jingyu Ke; Yanju Chen; Dahlia Malkhi; Yu Feng 001 (IACR Cryptol. ePrint Arch., 2025)