Demo Data from VLDB 2026 / reviewers in the wild / expert
Tamir Heyman
dblp:64/6178
· DBLP profile ↗
15ranked-venue papers
3as first author
0since 2021 · last 2014
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 12 · 3 first-authorSoftware engineering, systems software and programming languages · 8 · 1 first-authorArtificial intelligence and machine learning · 1 · 1 first-authorSystems, architecture and hardware · 1
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Computer architecture, parallel and distributed computing, and storage systems
3 papers |
Electronic design automation · 74% Parallel and multicore computing · 26% | |
| Theoretical computer science
3 papers |
Automated reasoning and model checking · 92% Logic in computer science · 8% |
Topics — the 10 heaviest of 10, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Electronic design automation › hardware verification and test
hardware verification |
0.1 | 2 | 2000 | Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits · CAV 2000 Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists · CAV 1999 |
Automated reasoning and model checking
model checking |
0.0 | 2 | 2001 | Distributed Symbolic Model Checking for µ-Calculus · CAV 2001 RuleBase: Model Checking at IBM · CAV 1997 |
Automated reasoning and model checking
reachability |
0.0 | 1 | 2003 | A Work-Efficient Distributed Algorithm for Reachability Analysis · CAV 2003 |
Parallel and multicore computing › parallel computing › parallel program analysis
parallel verification |
0.0 | 1 | 2000 | Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits · CAV 2000 |
Electronic design automation › hardware verification and test › formal verification
reachability analysis |
0.0 | 1 | 2000 | Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits · CAV 2000 |
Electronic design automation
model checking |
0.0 | 1 | 1999 | Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists · CAV 1999 |
Automated reasoning and model checking › model checking
symbolic model checking |
0.0 | 1 | 1997 | RuleBase: Model Checking at IBM · CAV 1997 |
Parallel and multicore computing › parallel algorithms
work-efficient parallel algorithms |
0.0 | 1 | 2003 | A Work-Efficient Distributed Algorithm for Reachability Analysis · CAV 2003 |
Logic in computer science › modal logic › multi-modal logic
modal mu-calculus |
0.0 | 1 | 2001 | Distributed Symbolic Model Checking for µ-Calculus · CAV 2001 |
Electronic design automation › hardware verification and test › functional verification
logic verification |
0.0 | 1 | 2000 | Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits · CAV 2000 |
Methods — techniques the papers use, named apart from their topics
parallelization · 0.0model checking · 0.0abstraction · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2014 | Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
Tamir Heyman, Dan Smith, Yogesh Mahajan, Lance Leong, Husam Abu-Haimed |
SAT | 1 |
| 2007 | Deeper Bound in BMC by Combining Constant Propagation and AbstractionabstractThe most successful technologies for automatic verification of large industrial circuits are bounded model checking, abstraction, and iterative refinement. Previous work has demonstrated the ability to verify circuits with thousands of state elements achieving bounds of at most a couple of hundreds. In this paper we present several novel techniques for abstraction-based bounded model checking. Specifically, we introduce a constant-propagation technique to simplify the formulas submitted to the CNF SAT solver; we present a new proof-based iterative abstraction technique for bounded model checking; and we show how the two techniques can be combined. The experimental results demonstrate our ability to handle circuit with several thousands state elements reaching bounds nearing 1,000. Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Y. Vardi, Yakir Vizel, Yael Zbar |
ASP-DAC | 4 |
| 2006 | A work-efficient distributed algorithm for reachability analysis
Orna Grumberg, Tamir Heyman, Assaf Schuster |
Formal Methods Syst. Des. | 2 |
| 2005 | Verifying Very Large Industrial Circuits Using 100 Processes and Beyond
Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster |
ATVA | 4 |
| 2005 | Distributed Symbolic Model Checking for µ-Calculus
Orna Grumberg, Tamir Heyman, Assaf Schuster |
Formal Methods Syst. Des. | 2 |
| 2003 | A Work-Efficient Distributed Algorithm for Reachability Analysis
Orna Grumberg, Tamir Heyman, Assaf Schuster |
CAV | 2 |
| 2003 | An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists
Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz |
Formal Methods Syst. Des. | 2 |
| 2003 | Scalable distributed on-the-fly symbolic model checking
Shoham Ben-David, Orna Grumberg, Tamir Heyman, Assaf Schuster |
Int. J. Softw. Tools Technol. Transf. | 3 |
| 2002 | A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits
Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster |
Formal Methods Syst. Des. | 1 |
| 2001 | Distributed Symbolic Model Checking for µ-Calculus
Orna Grumberg, Tamir Heyman, Assaf Schuster |
CAV | 2 |
| 2001 | 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. | 6 |
| 2000 | Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits
Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster |
CAV | 1 |
| 2000 | Scalable Distributed On-the-Fly Symbolic Model Checking
Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster |
FMCAD | 2 |
| 1999 | Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists
Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz |
CAV | 2 |
| 1997 | 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 | 6 |