Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity. - Kiyoharu Hamaguchi; Hiromi Hiraishi; Shuzo Yajima (CAV, 1990)

Vectorized Model Checking for Computation Tree Logic. - Hiromi Hiraishi; Shintaro Meki; Kiyoharu Hamaguchi (CAV, 1990)

Formal Verification of Speed-Dependent Asynchronous Cicuits Using Symbolic Model Checking of branching Time Regular Temporal Logic. - Kiyoharu Hamaguchi; Hiromi Hiraishi; Shuzo Yajima (CAV, 1991)

Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification. - Hiromi Hiraishi; Kiyoharu Hamaguchi; Hiroyuki Ochi; Shuzo Yajima (CAV, 1991)

Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic. - Kiyoharu Hamaguchi; Hiromi Hiraishi; Shuzo Yajima (CAV, 1992)

Infinity-Regular Temporal Logic and its Model Checking Problem. - Kiyoharu Hamaguchi; Hiromi Hiraishi; Shuzo Yajima (Theor. Comput. Sci., 1992)

The Complexity of the Optimal Variable Ordering Problems of Shared Binary Decision Diagrams. - Seiichiro Tani; Kiyoharu Hamaguchi; Shuzo Yajima (ISAAC, 1993)

Efficient construction of binary moment diagrams for verifying arithmetic circuits. - Kiyoharu Hamaguchi; Akihito Morita; Shuzo Yajima (ICCAD, 1995)

Another Look at LTL Model Checking. - Edmund M. Clarke; Orna Grumberg; Kiyoharu Hamaguchi (Formal Methods Syst. Des., 1997)

Ordered Quantum Branching Programs Are More Powerful than Ordered Probabilistic Branching Programs under a Bounded-Width Restriction. - Masaki Nakanishi; Kiyoharu Hamaguchi; Toshinobu Kashiwabara (COCOON, 2000)

Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs. - Kiyoharu Hamaguchi; Hidekazu Urushihara; Toshinobu Kashiwabara (FMCAD, 2000)

Symbolic simulation heuristics for high-level design descriptions with uninterpreted functions. - Kiyoharu Hamaguchi (HLDVT, 2001)

Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas. - Atsushi Moritomo; Kiyoharu Hamaguchi; Toshinobu Kashiwabara (ATVA, 2004)

Symbolic Simulation Heuristics for High-Level Hardware Descriptions Including Uninterpreted Functions. - Kiyoharu Hamaguchi (IEICE Trans. Inf. Syst., 2004)

Automatic monitor generation from regular expression based specifications for module interface verification. - Yosuke Kakiuchi; A. Kitajima; Kiyoharu Hamaguchi; Toshinobu Kashiwabara (ISCAS (4), 2005)

Expressive Power of Quantum Pushdown Automata with Classical Stack Operations under the Perfect-Soundness Condition. - Masaki Nakanishi; Kiyoharu Hamaguchi; Toshinobu Kashiwabara (IEICE Trans. Inf. Syst., 2006)

Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints. - Hiroaki Kozawa; Kiyoharu Hamaguchi; Toshinobu Kashiwabara (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2007)

Checker Generation of Assertions with Local Variables for Model Checking. - Sho Takeuchi; Kiyoharu Hamaguchi; Toshinobu Kashiwabara (IPSJ Trans. Syst. LSI Des. Methodol., 2009)

Approximate Model Checking Using a Subset of First-order Logic. - Kiyoharu Hamaguchi; Kazuya Masuda; Toshinobu Kashiwabara (IPSJ Trans. Syst. LSI Des. Methodol., 2010)

Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic. - Hiroaki Shimizu; Kiyoharu Hamaguchi; Toshinobu Kashiwabara (IPSJ Trans. Syst. LSI Des. Methodol., 2010)

Symbolic Discord Computation for Efficient Analysis of Message Sequence Charts. - Yosuke Kakiuchi; Tomofumi Nakagawa; Kiyoharu Hamaguchi; Tadaaki Tanimoto; Masaki Nakanishi (IPSJ Trans. Syst. LSI Des. Methodol., 2011)

Coverage-Driven Design Verification Using a Diverse SAT Solver. - Yosuke Kakiuchi; Kiyoharu Hamaguchi (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2017)

Extracting hardware assertions including word-level relations over multiple clock cycles. - Mami Miyamoto; Kiyoharu Hamaguchi (ISQED, 2018)

Applying an SMT Solver to Coverage-Driven Design Verification. - Kiyoharu Hamaguchi (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2018)

Foreword. - Kiyoharu Hamaguchi (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2019)

Parallelizing Random and SAT-based Verification Processes for Improving Toggle Coverage. - Kiyoharu Hamaguchi (IPSJ Trans. Syst. LSI Des. Methodol., 2023)