Data Compression of the Kanji Character Patterns Digitized on the Hexagonal Mesh. - Shuzo Yajima; Jan L. Goodsell; Takao Ichida; Hiromi Hiraishi (IEEE Trans. Pattern Anal. Mach. Intell., 1981)

Algebraic Specification of Parallel Systems Based on Binary Relations between Events. - Shigeharu Teshima; Hiromi Hiraishi; Shuzo Yajima (Syst. Comput. Jpn., 1988)

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)

Computing Quantitative Characteristics of Finite-State Real-Time Systems. - Sérgio Vale Aguiar Campos; Edmund M. Clarke; Wilfredo R. Marrero; Marius Minea; Hiromi Hiraishi (RTSS, 1994)

Verification of the Futurebus+ Cache Coherence Protocol. - Edmund M. Clarke; Orna Grumberg; Hiromi Hiraishi; Somesh Jha; David E. Long; Kenneth L. McMillan; Linda A. Ness (Formal Methods Syst. Des., 1995)

Temporal Verification of Real-Time Systems. - Sérgio Vale Aguiar Campos; Edmund M. Clarke; Wilfredo R. Marrero; Marius Minea; Hiromi Hiraishi (IEICE Trans. Inf. Syst., 1995)

Towards Verification of Bit-Slice Circuits-Time-Space Modal Model Checking Approach-. - Hiromi Hiraishi (IEICE Trans. Inf. Syst., 1995)

Formal Verification Of Self-Testing Properties Of Combinational Circuits. - Kazuo Kawakubo; Koji Tanaka; Hiromi Hiraishi (Asian Test Symposium, 1996)

Verification of deadlock free property of high level robot control. - Hiromi Hiraishi (Asian Test Symposium, 2000)

Yet more image computations for SMV, the symbolic model verifier. - Hiromi Hiraishi (Syst. Comput. Jpn., 2000)