CLEO: a CMOS layout generator. - Antun Domic; Samuel Levitin; Nathan Phillips; Channeary Thai; Thomas R. Shiple; Dilip Bhavsar; Clint Bissel (ICCAD, 1989)

Automatic Reduction in CTL Compositional Model Checking. - Thomas R. Shiple; Massimiliano Chiodo; Alberto L. Sangiovanni-Vincentelli; Robert K. Brayton (CAV, 1992)

Automatic compositional minimization in CTL model checking. - Massimiliano Chiodo; Thomas R. Shiple; Alberto L. Sangiovanni-Vincentelli; Robert K. Brayton (ICCAD, 1992)

A Unified Approach to Language Containment and Fair CTL Model Checking. - Ramin Hojati; Thomas R. Shiple; Robert K. Brayton; Robert P. Kurshan (DAC, 1993)

Formula-Dependent Equivalence for Compositional CTL Model Checking. - Adnan Aziz; Thomas R. Shiple; Vigyan Singhal (CAV, 1994)

HSIS: A BDD-Based Environment for Formal Verification. - Adnan Aziz; Felice Balarin; Szu-Tsung Cheng; Ramin Hojati; Timothy Kam; Sriram C. Krishnan; Rajeev K. Ranjan 001; Thomas R. Shiple; Vigyan Singhal; Serdar Tasiran; Huey-Yih Wang; Robert K. Brayton; et al. (DAC, 1994)

Heuristic Minimization of BDDs Using Don't Cares. - Thomas R. Shiple; Ramin Hojati; Alberto L. Sangiovanni-Vincentelli; Robert K. Brayton (DAC, 1994)

Two-phase Logic Design by Hardware Flowcharts. - Kevin Covey; Sandra Murdock; Thomas R. Shiple (ICCD, 1994)

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)

Constructive Analysis of Cyclic Circuits. - Thomas R. Shiple; Gérard Berry; Hervé J. Touati (ED&TC, 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)

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)

Approximation and Decomposition of Binary Decision Diagrams. - Kavita Ravi; Kenneth L. McMillan; Thomas R. Shiple; Fabio Somenzi (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)

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)

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)

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)

Formula-Dependent Equivalence for Compositional CTL Model Checking. - Adnan Aziz; Thomas R. Shiple; Vigyan Singhal; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (Formal Methods Syst. Des., 2002)

Multi-mode redundancy removal. - Stephen M. Plaza; Prashant Saxena; Thomas R. Shiple; Pei-Hsin Ho (ISQED, 2011)

Constructive Boolean circuits and the exactness of timed ternary simulation. - Michael Mendler; Thomas R. Shiple; Gérard Berry (Formal Methods Syst. Des., 2012)