Our expertise covers a wide spectrum of technologies in the space of hardware and software verification, automated reasoning, networking and cloud computing.
With our vast expertise in verification technologies, we support IBM product teams and participate in research activities that advance automated reasoning science and cloud computing technology.
Shai Doron,
Manager, Formal Quality Technologies,
IBM Research - Haifa
Publications
Author | Title | Conference/Journal | Year | |
---|---|---|---|---|
R. Gal, H. Kermany, A. Ivrii, Z. Nevo, A. Ziv | Late breaking results: Friends - finding related interesting events via neighbor detection | Design Automation Conference, (DAC) 2020 | 2020 | Link |
Rohit Dureja; Jason Baumgartner; Robert Kanzelman; Mark Williams; Kristin Y. Rozier | Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration | FMCAD 2020 | 2020 | Link |
Raj Kumar Gajavelly, Jason Baumgartner, Alexander Ivrii, Robert L. Kanzelman, Shiladitya Ghosh | Input Elimination Transformations for Scalable Verification and Trace Reconstruction | FMCAD 2019 | 2019 | Link |
Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman, Kristin Y. Rozier | Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties | FMCAD 2019 | 2019 | Link |
Ryan Berryhill, Alexander Ivrii, Andreas G. Veneris | Finding All Minimal Safe Inductive Sets | SAT 2018 | 2018 | Link |
Alexander Ivrii, Ziv Nevo, Jason Baumgartner | k-FAIR = k-LIVENESS + FAIR Revisiting SAT-based Liveness Algorithms | FMCAD 2018 | 2018 | Link |
Ryan Berryhill, Alexander Ivrii, Neil Veira and Andreas Veneris | Learning Support Sets in IC3 and Quip: the Good, the Bad, and the Ugly | FMCAD | 2017 | Link |
Arie Gurfinkel and Alexander Ivrii | K-Induction without Unrolling | FMCAD | 2017 | Link |
Pradeep Kumar Nalla, Raj Kumar Gajavelly, Jason Baumgartner, Hari Mony, Robert Kanzelman, Alexander Ivrii | The Art of Semi-Formal Bug Hunting | ICCAD | 2016 | Link |
S. Bergman, G. Bobok, W. Kowalski, S. Koyfman, S. Moran, Z. Nevo, A. Orni, V. Paruthi, W. Roesner, G. Shurek, V. Vuyyuru | Designer-Level Verification – an Industrial Experience Story | DATE 2015 | 2015 | Link |
Arie Gurfinkel, Alexander Ivrii | Pushing to the Top | FMCAD | 2015 | Link |
Alexander Ivrii, Arie Gurfinkel and Anton Belov | Small Inductive Safe Invariants | Formal Methods in Computer-Aided Design | 2014 | Link |
Gadi Aleksandrowicz, Alexander Ivrii, Oded Margalit, and Dan Rasin | Generating Linear Invariants for Model Checking | Haifa Verification Conference | 2014 | |
U. Krautz, V. Paruthi, A. Arunagiri, S. Kumar, S. Pujar, T. Babinsky | Automatic Verification of Floating Point Units | Design Automation Conference | 2014 | Link |
A. Lvov, L. A. Lastras-Montaño, B. Trager, V. Paruthi, R. Shadowen, A. El-Zein | Verification of Galois Field Based Circuits by Formal Reasoning Based on Computational Algebraic Geometry | Formal Methods in System Design | 2014 | Link |
J. Xu, M. Williams, H. Mony, J. Baumgartner | Scalable reachability analysis via automated dynamic netlist-based hint generation | Journal of Formal Methods in System Design | 2014 | Link |
P.K. Nalla, R.J. Gajavelly, H. Mony, J. Baumgartner, R. Kanzelman | Effective Liveness Verification Using a Transformation-Based Framework | VLSI Design | 2014 | Link |
A. Mishchenko, N. Eén, R. K. Brayton, J. Baumgartner, H. Mony, P.K. Nalla | GLA: gate-level abstraction revisited | Design Automation and Test in Europe | 2013 | Link |
G. Aleksandrowicz, J. Baumgartner, A. Ivrii, Z. Nevo | Generalized counterexamples to liveness properties | Formal Methods in Computer-Aided Design | 2013 | Link |
H. Chockler, A. Ivrii, A. Matsliah, S.F. Rollini, N. Sharygina | Using cross-entropy for satisfiability | Symposium on Applied Computing | 2013 | Link |
J. Xu, M. Williams, H. Mony, J. Baumgartner | Enhanced reachability analysis via automated dynamic netlist-based hint generation | Formal Methods in Computer-Aided Design | 2012 | Link |
J. Baumgartner, A. Ivrii, A. Matsliah, H. Mony | IC3-guided abstraction | Formal Methods in Computer-Aided Design | 2012 | Link |
A. Lvov, L.A. Lastras-Montano, V. Paruthi, R. Shadowen, A. El-Zein | Formal verification of error correcting circuits using computational algebraic geometry | Formal Methods in Computer-Aided Design | 2012 | Link |
A. Belov, A. Ivrii, A. Matsliah, J. Marques-Silva | On Efficient Computation of Variable MUSes | Sat | 2012 | Link |
A. Matsliah, A. Sabharwal, H. Samulowitz | Augmenting Clause Learning with Implied Literals | Sat | 2012 | Link |
H. Chockler, A. Ivrii, A. Matsliah | Computing Interpolants without Proofs | Haifa Verification Conference | 2012 | Link |
Y. Ben-Haim, A. Ivrii, O. Margalit, A. Matsliah | Perfect Hashing and CNF Encodings of Cardinality Constraints | Sat | 2012 | Link |
H. Chockler, A. Ivrii, A. Matsliah, S. Moran, Z. Nevo | Incremental formal verification of hardware | Formal Methods in Computer-Aided Design | 2011 | Link |
K.D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, M. Behm, A. Ziv, J. Schumann, C. Meissner, J. Koesters, J. Hsu, B. Brock | Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems | IBM Journal of Research and Development | 2011 | Link |
M. L. Case, J. Baumgartner, H. Mony and R. L. Kanzelman | Optimal redundancy removal without fixedpoint computation | Formal Methods in Computer Aided Design | 2011 | Link |
M. L. Case, J. Baumgartner, H. Mony and R. L. Kanzelman | Approximate reachability with combined symbolic and ternary simulation | Formal Methods in Computer Aided Design | 2011 | Link |
J. Sawada, P. Sandon, V. Paruthi, J. Baumgartner, M. L. Case and H. Mony | Hybrid verification of a hardware modular reduction engine | Formal Methods in Computer Aided Design | 2011 | Link |
V. Paruthi | Large-scale Application of Formal Verification: From Fiction to Fact | Formal Methods in Computer-Aided Design | 2010 | Link |
G. Auerbach, F. Copty, V.Paruthi | Formal Verification of Arbiters using Property Strengthening and Underapproximations | Formal Methods in Computer-Aided Design | 2010 | Link |
J. Baumgartner, M. L. Case and H. Mony | Coping with Moore's Law (and More): Supporting Arrays in State-of-the-Art Model Checkers | Formal Methods in Computer Aided Design | 2010 | Link |