A symbolic algorithm for low-power sequential synthesis. - Balakrishna Kumthekar; In-Ho Moon; Fabio Somenzi (ISLPED, 1997)

Approximate reachability don't cares for CTL model checking. - In-Ho Moon; Jae-Young Jang; Gary D. Hachtel; Fabio Somenzi; Jun Yuan 007; Carl Pixley (ICCAD, 1998)

Least fixpoint approximations for reachability analysis. - In-Ho Moon; James H. Kukula; Thomas R. Shiple; Fabio Somenzi (ICCAD, 1999)

To split or to conjoin: the question in image computation. - In-Ho Moon; James H. Kukula; Kavita Ravi; Fabio Somenzi (DAC, 2000)

Iterative Abstraction-Based CTL Model Checking. - Jae-Young Jang; In-Ho Moon; Gary D. Hachtel (DATE, 2000)

Border-Block Triangular Form and Conjunction Schedule in Image Computation. - In-Ho Moon; Gary D. Hachtel; Fabio Somenzi (FMCAD, 2000)

Simplifying Circuits for Formal Verification Using Parametric Representation. - In-Ho Moon; Hee-Hwan Kwak; James H. Kukula; Thomas R. Shiple; Carl Pixley (FMCAD, 2002)

Combinational equivalence checking through function transformation. - Hee-Hwan Kwak; In-Ho Moon; James H. Kukula; Thomas R. Shiple (ICCAD, 2002)

Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders. - In-Ho Moon; Carl Pixley (FMCAD, 2004)

Practical Issues in Sequential Equivalence Checking through Alignability: Handling Don't Cares and Generating Debug Traces. - In-Ho Moon; Per Bjesse; Carl Pixley (HLDVT, 2006)

A compositional approach to the combination of combinational and sequential equivalence checking of circuits without known reset states. - In-Ho Moon; Per Bjesse; Carl Pixley (DATE, 2007)

Compositional verification of retiming and sequential optimizations. - In-Ho Moon (DAC, 2008)

Learning from Constraints for Formal Property Checking. - In-Ho Moon; Kevin Harer (J. Electron. Test., 2010)

Abstraction-Based Livelock/Deadlock Checking for Hardware Verification. - In-Ho Moon; Kevin Harer (DIFTS@FMCAD, 2013)