| 2008 | ATVA | Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic. | Hiroaki Shimizu, Kiyoharu Hamaguchi, Toshinobu Kashiwabara |
| 2005 | ISCAS | Automatic monitor generation from regular expression based specifications for module interface verification. | Yosuke Kakiuchi, A. Kitajima, Kiyoharu Hamaguchi, Toshinobu Kashiwabara |
| 2004 | ATVA | Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas. | Atsushi Moritomo, Kiyoharu Hamaguchi, Toshinobu Kashiwabara |
| 2000 | COCOON | Ordered Quantum Branching Programs Are More Powerful than Ordered Probabilistic Branching Programs under a Bounded-Width Restriction. | Masaki Nakanishi, Kiyoharu Hamaguchi, Toshinobu Kashiwabara |
| 2000 | FMCAD | Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs. | Kiyoharu Hamaguchi, Hidekazu Urushihara, Toshinobu Kashiwabara |
| 1995 | ICCAD | Efficient construction of binary moment diagrams for verifying arithmetic circuits. | Kiyoharu Hamaguchi, Akihito Morita, Shuzo Yajima |
| 1994 | CAV | Another Look at LTL Model Checking. | Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi |
| 1993 | ISAAC | The Complexity of the Optimal Variable Ordering Problems of Shared Binary Decision Diagrams. | Seiichiro Tani, Kiyoharu Hamaguchi, Shuzo Yajima |
| 1992 | CAV | Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic. | Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yajima |
| 1991 | CAV | Formal Verification of Speed-Dependent Asynchronous Cicuits Using Symbolic Model Checking of branching Time Regular Temporal Logic. | Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yajima |
| 1991 | CAV | Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification. | Hiromi Hiraishi, Kiyoharu Hamaguchi, Hiroyuki Ochi, Shuzo Yajima |
| 1990 | CAV | Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity. | Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yajima |
| 1990 | CAV | Vectorized Model Checking for Computation Tree Logic. | Hiromi Hiraishi, Shintaro Meki, Kiyoharu Hamaguchi |