Object relocation in OX. - James H. Kukula (ICCD, 1988)

Finite State Machine Decomposition by Transition Pairing. - James H. Kukula; Srinivas Devadas (ICCAD, 1991)

Bitwise Encoding of Finite State Machines. - José Monteiro 001; James H. Kukula; Srinivas Devadas; Horácio C. Neto (VLSI Design, 1994)

A Comparison of Presburger Engines for EFSM Reachability. - Thomas R. Shiple; James H. Kukula; Rajeev K. Ranjan 001 (CAV, 1998)

Hybrid Verification Using Saturated Simulation. - Adnan Aziz; James H. Kukula; Thomas R. Shiple (DAC, 1998)

Techniques for Implicit State Enumeration of EFSMs. - James H. Kukula; Thomas R. Shiple; Adnan Aziz (FMCAD, 1998)

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

Building Circuits from Relations. - James H. Kukula; Thomas R. Shiple (CAV, 2000)

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

Smart Simulation Using Collaborative Formal and Simulation Engines. - Pei-Hsin Ho; Thomas R. Shiple; Kevin Harer; James H. Kukula; Robert F. Damiano; Valeria Bertacco; Jerry Taylor; Jiang Long (ICCAD, 2000)

Using Combinatorial Optimization Methods for Quantification Scheduling. - Pankaj Chauhan; Edmund M. Clarke; Somesh Jha; James H. Kukula; Helmut Veith; Dong Wang (CHARME, 2001)

Symbolic RTL Simulation. - Alfred Kölbl; James H. Kukula; Robert F. Damiano (DAC, 2001)

Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines. - Dong Wang; Pei-Hsin Ho; Jiang Long; James H. Kukula; Yunshan Zhu; Hi-Keung Tony Ma; Robert F. Damiano (DAC, 2001)

Using cutwidth to improve symbolic simulation and Boolean satisfiability. - Dong Wang; Edmund M. Clarke; Yunshan Zhu; James H. Kukula (HLDVT, 2001)

Non-linear Quantification Scheduling in Image Computation. - Pankaj Chauhan; Edmund M. Clarke; Somesh Jha; James H. Kukula; Thomas R. Shiple; Helmut Veith; Dong Wang (ICCAD, 2001)

Efficient control state-space search. - Adnan Aziz; James H. Kukula; Thomas R. Shiple; Jun Yuan 007 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001)

SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. - Edmund M. Clarke; Anubhav Gupta 001; James H. Kukula; Ofer Strichman (CAV, 2002)

Handling special constructs in symbolic simulation. - Alfred Kölbl; James H. Kukula; Kurt Antreich; Robert F. Damiano (DAC, 2002)

Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis. - Pankaj Chauhan; Edmund M. Clarke; James H. Kukula; Samir Sapra; Helmut Veith; Dong Wang (FMCAD, 2002)

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)

Checking satisfiability of a conjunction of BDDs. - Robert F. Damiano; James H. Kukula (DAC, 2003)

Generator-based Verification. - Yunshan Zhu; James H. Kukula (ICCAD, 2003)

Guiding SAT Diagnosis with Tree Decompositions. - Per Bjesse; James H. Kukula; Robert F. Damiano; Ted Stanion; Yunshan Zhu (SAT, 2003)

Using Counter Example Guided Abstraction Refinement to Find Complex Bugs. - Per Bjesse; James H. Kukula (DATE, 2004)

Automatic generalized phase abstraction for formal verification. - Per Bjesse; James H. Kukula (ICCAD, 2005)