Techniques for programmable logic array folding. - Gary D. Hachtel; A. Richard Newton; Alberto L. Sangiovanni-Vincentelli (DAC, 1982)

Implication algorithms for MOS switch level functional macromodeling implication and testing. - Michael R. Lightner; Gary D. Hachtel (DAC, 1982)

An Algorithm for Optimal PLA Folding. - Gary D. Hachtel; A. Richard Newton; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1982)

Logic Minimization Algorithms for VLSI Synthesis - Robert K. Brayton; Gary D. Hachtel; Curtis T. McMullen; Alberto L. Sangiovanni-Vincentelli (Springer, 1984)

A Theory and Algorithmic Frame for Switch Level Simulation. - Michael R. Lightner; Gary D. Hachtel; Richard H. Byrd; Michel Heydemann (IMACS European Simulation Meeting, 1984)

SOCRATES: a system for automatically synthesizing and optimizing combinational logic. - David Gregory; Karen A. Bartlett; Aart J. de Geus; Gary D. Hachtel (DAC, 1986)

Synthesis and Optimization of Multilevel Logic under Timing Constraints. - Karen A. Bartlett; William W. Cohen; Aart J. de Geus; Gary D. Hachtel (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1986)

BEATNP: a tool for partitioning Boolean networks. - Hyunwoo Cho; Gary D. Hachtel; M. Nash; L. Setiono (ICCAD, 1988)

Performance enhancements in BOLD using 'implications'. - Gary D. Hachtel; Reily M. Jacoby; P. Moceyunas; Christopher R. Morrison (ICCAD, 1988)

Multi-level logic minimization using implicit don't cares. - Karen A. Bartlett; Robert K. Brayton; Gary D. Hachtel; Reily M. Jacoby; Christopher R. Morrison; Richard L. Rudell; Alberto L. Sangiovanni-Vincentelli; Albert R. Wang (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1988)

Verification algorithms for VLSI synthesis. - Gary D. Hachtel; Reily M. Jacoby (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1988)

On optimal extraction of combinational logic and don't care sets from hardware description languages. - Glenn Colón-Bonet; Eric M. Schwarz; D. G. Bostick; Gary D. Hachtel; Michael R. Lightner (ICCAD, 1989)

On properties of algebraic transformation and the multifault testability of multilevel logic. - Gary D. Hachtel; Reily M. Jacoby; Kurt Keutzer; Christopher R. Morrison (ICCAD, 1989)

New ATPG techniques for logic optimization. - Reily M. Jacoby; P. Moceyunas; Hyunwoo Cho; Gary D. Hachtel (ICCAD, 1989)

Linear complexity algorithms for hierarchical routing. - Gary D. Hachtel; Christopher R. Morrison (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1989)

Results on the Interface between Formal Verification and ATPG. - Hyunwoo Cho; Gary D. Hachtel; Seh-Woong Jeong; Bernard Plessier; Eric M. Schwarz; Fabio Somenzi (CAV (DIMACS/AMS volume), 1990)

ATPG Aspects of FSM Verification. - Hyunwoo Cho; Gary D. Hachtel; Seh-Woong Jeong; Bernard Plessier; Eric M. Schwarz; Fabio Somenzi (ICCAD, 1990)

Multilevel logic synthesis. - Robert K. Brayton; Gary D. Hachtel; Alberto L. Sangiovanni-Vincentelli (Proc. IEEE, 1990)

Extended BDD's: Trading off Canonicity for Structure in Verification Algorithms. - Seh-Woong Jeong; Bernard Plessier; Gary D. Hachtel; Fabio Somenzi (ICCAD, 1991)

Variable Ordering and Selection for FSM Traversal. - Seon-Woong Jeong; Bernard Plessier; Gary D. Hachtel; Fabio Somenzi (ICCAD, 1991)

Don't Care Sequences and the Optimization of Interacting Finite State Machines. - June-Kyung Rho; Gary D. Hachtel; Fabio Somenzi (ICCAD, 1991)

Redundancy Identification and Removal Based on Implicit State Enumeration. - Hyunwoo Cho; Gary D. Hachtel; Fabio Somenzi (ICCD, 1991)

Fast Sequential ATPG Based on Implicit State Enumeration. - Hyunwoo Cho; Gary D. Hachtel; Fabio Somenzi (ITC, 1991)

MUSE: a multilevel symbolic encoding algorithm for state assignment. - Xuejun Du; Gary D. Hachtel; Bill Lin 001; A. Richard Newton (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1991)

Exact Calculation of Synchronization Sequences Based on Binary Decision Diagrams. - Carl Pixley; Seh-Woong Jeong; Gary D. Hachtel (DAC, 1992)

On properties of algebraic transformations and the synthesis of multifault-irredundant circuits. - Gary D. Hachtel; Reily M. Jacoby; Kurt Keutzer; Christopher R. Morrison (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1992)

Algorithms for Approximate FSM Traversal. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Bernard Plessier; Fabio Somenzi (DAC, 1993)

A symbolic algorithm for maximum flow in 0-1 networks. - Gary D. Hachtel; Fabio Somenzi (ICCAD, 1993)

Redundancy identification/removal and test generation for sequential circuits using implicit state enumeration. - Hyunwoo Cho; Gary D. Hachtel; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1993)

Probabilistic Analysis of Large Finite State Machines. - Gary D. Hachtel; Enrico Macii; Abelardo Pardo; Fabio Somenzi (DAC, 1994)

Timing Analysis of Combinational Circuits using ADD's. - R. Iris Bahar; Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Fabio Somenzi (EDAC-ETC-EUROASIC, 1994)

A State Space Decomposition Algorithm for Approximate FSM Traversal. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Massimo Poncino; Fabio Somenzi (EDAC-ETC-EUROASIC, 1994)

Symbolic Algorithms to Calculate Steady-State Probabilities of a Finite State Machine. - Gary D. Hachtel; Enrico Macii; Abelardo Pardo; Fabio Somenzi (EDAC-ETC-EUROASIC, 1994)

An ADD-based algorithm for shortest path back-tracing of large graphs. - R. Iris Bahar; Gary D. Hachtel; Abelardo Pardo; Massimo Poncino; Fabio Somenzi (Great Lakes Symposium on VLSI, 1994)

A symbolic method to reduce power consumption of circuits containing false paths. - R. Iris Bahar; Gary D. Hachtel; Enrico Macii; Fabio Somenzi (ICCAD, 1994)

Re-encoding sequential circuits to reduce power dissipation. - Gary D. Hachtel; Mariano Hermida de la Rica; Abelardo Pardo; Massimo Poncino; Fabio Somenzi (ICCAD, 1994)

A Structural Approach to State Space Decomposition for Approximate Reachability Analysis. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Massimo Poncino; Fabio Somenzi (ICCD, 1994)

Extended BDDs: Trading off Canonicity for Structure in Verification Algorithms. - Bernard Plessier; Gary D. Hachtel; Fabio Somenzi (Formal Methods Syst. Des., 1994)

Exact calculation of synchronizing sequences based on binary decision diagrams. - Carl Pixley; Seh-Woong Jeong; Gary D. Hachtel (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994)

Exact and heuristic algorithms for the minimization of incompletely specified state machines. - June-Kyung Rho; Gary D. Hachtel; Fabio Somenzi; Reily M. Jacoby (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994)

Computing the Maximum Power Cycles of a Sequential Circuit. - Srilatha Manne; Abelardo Pardo; R. Iris Bahar; Gary D. Hachtel; Fabio Somenzi; Enrico Macii; Massimo Poncino (DAC, 1995)

CMOS dynamic power estimation based on collapsible current source transistor modeling. - Abelardo Pardo; R. Iris Bahar; Srilatha Manne; Peter Feldmann; Gary D. Hachtel; Fabio Somenzi (ISLPD, 1995)

Logic synthesis and verification algorithms. - Gary D. Hachtel; Fabio Somenzi (Kluwer, 1996)

VIS: A System for Verification and Synthesis. - Robert K. Brayton; Gary D. Hachtel; Alberto L. Sangiovanni-Vincentelli; Fabio Somenzi; Adnan Aziz; Szu-Tsung Cheng; Stephen A. Edwards; Sunil P. Khatri; Yuji Kukimoto; Abelardo Pardo; Shaz Qadeer; Rajeev K. Ranjan 001; et al. (CAV, 1996)

VIS. - Robert K. Brayton; Gary D. Hachtel; Alberto L. Sangiovanni-Vincentelli; Fabio Somenzi; Adnan Aziz; Szu-Tsung Cheng; Stephen A. Edwards; Sunil P. Khatri; Yuji Kukimoto; Abelardo Pardo; Shaz Qadeer; Rajeev K. Ranjan 001; et al. (FMCAD, 1996)

Modular Verification of Multipliers. - Kavita Ravi; Abelardo Pardo; Gary D. Hachtel; Fabio Somenzi (FMCAD, 1996)

Tearing based automatic abstraction for CTL model checking. - Woohyuk Lee; Abelardo Pardo; Jae-Young Jang; Gary D. Hachtel; Fabio Somenzi (ICCAD, 1996)

Symbolic computation of logic implications for technology-dependent low-power synthesis. - R. Iris Bahar; M. Burns; Gary D. Hachtel; Enrico Macii; H. Shin; Fabio Somenzi (ISLPED, 1996)

Automatic state space decomposition for approximate FSM traversal based on circuit analysis. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Massimo Poncino; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1996)

Algorithms for approximate FSM traversal based on state space decomposition. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Bernard Plessier; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1996)

Markovian analysis of large finite state machines. - Gary D. Hachtel; Enrico Macii; Abelardo Pardo; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1996)

Automatic Abstraction Techniques for Propositional µ-calculus Model Checking. - Abelardo Pardo; Gary D. Hachtel (CAV, 1997)

Algebraic Decision Diagrams and Their Applications. - R. Iris Bahar; Erica A. Frohm; Charles M. Gaona; Gary D. Hachtel; Enrico Macii; Abelardo Pardo; Fabio Somenzi (Formal Methods Syst. Des., 1997)

A Symbolic Algorithms for Maximum Flow in 0-1 Networks. - Gary D. Hachtel; Fabio Somenzi (Formal Methods Syst. Des., 1997)

Symbolic timing analysis and resynthesis for low power of combinational circuits containing false paths. - R. Iris Bahar; Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997)

Incremental CTL Model Checking Using BDD Subsetting. - Abelardo Pardo; Gary D. Hachtel (DAC, 1998)

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)

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)

Divide and Compose: SCC Refinement for Language Emptiness. - Chao Wang 001; Roderick Bloem; Gary D. Hachtel; Kavita Ravi; Fabio Somenzi (CONCUR, 2001)

Sharp Disjunctive Decomposition for Language Emptiness Checking. - Chao Wang 001; Gary D. Hachtel (FMCAD, 2002)

The Compositional Far Side of Image Computation. - Chao Wang 001; Gary D. Hachtel; Fabio Somenzi (ICCAD, 2003)

Improving Ariadneýs Bundle by Following Multiple Threads in Abstraction Refinement. - Chao Wang 001; Bing Li; HoonSang Jin; Gary D. Hachtel; Fabio Somenzi (ICCAD, 2003)

Refining the SAT decision ordering for bounded model checking. - Chao Wang 001; HoonSang Jin; Gary D. Hachtel; Fabio Somenzi (DAC, 2004)

Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking. - Chao Wang 001; Gary D. Hachtel; Fabio Somenzi (ICCD, 2004)

Logic synthesis and verification algorithms. - Gary D. Hachtel; Fabio Somenzi (Springer, 2006)

Compositional SCC Analysis for Language Emptiness. - Chao Wang 001; Roderick Bloem; Gary D. Hachtel; Kavita Ravi; Fabio Somenzi (Formal Methods Syst. Des., 2006)

Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement. - Chao Wang 001; Bing Li; HoonSang Jin; Gary D. Hachtel; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2006)

Abstraction Refinement for Large Scale Model Checking - Chao Wang 001; Gary D. Hachtel; Fabio Somenzi (Springer, 2006)