| 2013 | FMCAD | Abstraction-Based Livelock/Deadlock Checking for Hardware Verification. | In-Ho Moon, Kevin Harer |
| 2008 | DAC | Compositional verification of retiming and sequential optimizations. | In-Ho Moon |
| 2007 | DATE | 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 |
| 2004 | FMCAD | Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders. | In-Ho Moon, Carl Pixley |
| 2002 | FMCAD | Simplifying Circuits for Formal Verification Using Parametric Representation. | In-Ho Moon, Hee-Hwan Kwak, James H. Kukula, Thomas R. Shiple, Carl Pixley |
| 2002 | ICCAD | Combinational equivalence checking through function transformation. | Hee-Hwan Kwak, In-Ho Moon, James H. Kukula, Thomas R. Shiple |
| 2000 | DAC | To split or to conjoin: the question in image computation. | In-Ho Moon, James H. Kukula, Kavita Ravi, Fabio Somenzi |
| 2000 | DATE | Iterative Abstraction-Based CTL Model Checking. | Jae-Young Jang, In-Ho Moon, Gary D. Hachtel |
| 2000 | FMCAD | Border-Block Triangular Form and Conjunction Schedule in Image Computation. | In-Ho Moon, Gary D. Hachtel, Fabio Somenzi |
| 1999 | ICCAD | Least fixpoint approximations for reachability analysis. | In-Ho Moon, James H. Kukula, Thomas R. Shiple, Fabio Somenzi |
| 1998 | ICCAD | Approximate reachability don't cares for CTL model checking. | In-Ho Moon, Jae-Young Jang, Gary D. Hachtel, Fabio Somenzi, Jun Yuan, Carl Pixley |
| 1997 | ISLPED | A symbolic algorithm for low-power sequential synthesis. | Balakrishna Kumthekar, In-Ho Moon, Fabio Somenzi |