RuleBase: Model Checking at IBM. - Ilan Beer; Shoham Ben-David; Cindy Eisner; Daniel Geist; Leonid Gluhovsky; Tamir Heyman; Avner Landver; P. Paanah; Yoav Rodeh; G. Ronin; Yaron Wolfsthal (CAV, 1997)

Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists. - Jason Baumgartner; Tamir Heyman; Vigyan Singhal; Adnan Aziz (CAV, 1999)

Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. - Tamir Heyman; Daniel Geist; Orna Grumberg; Assaf Schuster (CAV, 2000)

On the Effective Deployment of Functional Formal Verification. - Yael Abarbanel-Vinov; Neta Aizenbud-Reshef; Ilan Beer; Cindy Eisner; Daniel Geist; Tamir Heyman; Iris Reuveni; Eran Rippel; Irit Shitsevalov; Yaron Wolfsthal; Tali Yatzkar-Haham (Formal Methods Syst. Des., 2001)

A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits. - Tamir Heyman; Daniel Geist; Orna Grumberg; Assaf Schuster (Formal Methods Syst. Des., 2002)

An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists. - Jason Baumgartner; Tamir Heyman; Vigyan Singhal; Adnan Aziz (Formal Methods Syst. Des., 2003)

Scalable distributed on-the-fly symbolic model checking. - Shoham Ben-David; Orna Grumberg; Tamir Heyman; Assaf Schuster (Int. J. Softw. Tools Technol. Transf., 2003)

Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation. - Orna Grumberg; Tamir Heyman; Nili Ifergan; Assaf Schuster (CHARME, 2005)

Distributed Symbolic Model Checking for µ-Calculus. - Orna Grumberg; Tamir Heyman; Assaf Schuster (Formal Methods Syst. Des., 2005)

A work-efficient distributed algorithm for reachability analysis. - Orna Grumberg; Tamir Heyman; Assaf Schuster (Formal Methods Syst. Des., 2006)

Deeper Bound in BMC by Combining Constant Propagation and Abstraction. - Roy Armoni; Limor Fix; Ranan Fraer; Tamir Heyman; Moshe Y. Vardi; Yakir Vizel; Yael Zbar (ASP-DAC, 2007)

Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. - Limor Fix; Orna Grumberg; Amnon Heyman; Tamir Heyman; Assaf Schuster (Int. J. Found. Comput. Sci., 2007)

Dominant Controllability Check Using QBF-Solver and Netlist Optimizer. - Tamir Heyman; Dan Smith; Yogesh Mahajan; Lance Leong; Husam Abu-Haimed (SAT, 2014)