Manifest Contracts for Datatypes. - Taro Sekiyama; Yuki Nishida 001; Atsushi Igarashi (POPL, 2015)

Sharper and Simpler Nonlinear Interpolants for Program Verification. - Takamasa Okudono; Yuki Nishida 001; Kensuke Kojima; Kohei Suenaga; Kengo Kido; Ichiro Hasuo (APLAS, 2017)

Nondeterministic Manifest Contracts. - Yuki Nishida 001; Atsushi Igarashi (PPDP, 2018)

Manifest Contracts with Intersection Types. - Yuki Nishida 001; Atsushi Igarashi (APLAS, 2019)

Compilation of Coordinated Choice. - Yuki Nishida 001; Atsushi Igarashi (CoRR, 2020)

Typed Software Contracts with Intersection and Nondeterminism. - Yuki Nishida 001 (2020)

Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types. - Yuki Nishida 001; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi (New Gener. Comput., 2022)

iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns. - Yuki Nishida 001; Kohei Suenaga; Atsushi Igarashi (ICBC, 2024)

Law and Order for Typestate with Borrowing. - Hannes Saffrich; Yuki Nishida 001; Peter Thiemann 001 (Proc. ACM Program. Lang., 2024)

Max-plus Algebraic Description of Evolutions of Weighted Timed Event Graphs. - Kensuke Kitai; Yuki Nishida 001; Yoshihide Watanabe (Theory Comput. Syst., 2024)

Algorithm for the CSR Expansion of Max-Plus Matrices Using the Characteristic Polynomial. - Yuki Nishida 001 (SIAM J. Discret. Math., 2025)

Combinatorial Algorithm for Tropical Linearly Factorized Programming. - Yuki Nishida 001 (CoRR, 2025)