RustHorn: CHC-based Verification for Rust Programs (full version). - Yusuke Matsushita 002; Takeshi Tsukada; Naoki Kobayashi 001 (CoRR, 2020)

RustHorn: CHC-based Verification for Rust Programs. - Yusuke Matsushita 002; Takeshi Tsukada; Naoki Kobayashi 001 (ACM Trans. Program. Lang. Syst., 2021)

RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. - Yusuke Matsushita 002; Xavier Denis; Jacques-Henri Jourdan; Derek Dreyer (PLDI, 2022)

Borrowable Fractional Ownership Types for Verification. - Takashi Nakayama; Yusuke Matsushita 002; Ken Sakayori; Ryosuke Sato 001; Naoki Kobayashi 001 (VMCAI (2), 2024)

SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches. - Hiroyuki Deguchi 002; Go Kamoda; Yusuke Matsushita 002; Chihiro Taguchi; Kohei Suenaga; Masaki Waga; Sho Yokoi (ICLR, 2025)

Nola: Later-Free Ghost State for Verifying Termination in Iris. - Yusuke Matsushita 002; Takeshi Tsukada (Proc. ACM Program. Lang., 2025)