In our ongoing endeavor to develop the next generation of Hybrid Cloud Quality Technologies and capabilities that can meet the increasing needs of our customers, we are exploring new exciting directions, including:
- Cloud Quality: Tools to verify network policies, test functional quality, and check and ensure the resiliency of IBM cloud.
- AI Quality: Technology and methodology to assess the quality of successful machine learning solutions. This includes advanced bias and drift detection techniques.
- Coverage Directed Generation (CDG): Technology aiming to automate coverage closure by generating new test-templates to hit never-hit events.
Our expertise is built upon a strong legacy of high-quality research and development going back over 30 years, during which we pioneered several of the practices currently prevalent in the industry. Some of our prominent technologies include:
- Using constraint-solving capabilities for stimuli generation in the domain of functional verification of hardware. This includes separating the architecture description (model) from the generation engine.
- Scalable formal verification technology that employs state-of-the-art model checking algorithms with extensive support for all common design and specification languages, including PSL (an IEEE standard specification language conceived by our department).
- Powerful post-silicon validation aimed at finding intricate bugs that occur in complex multi-processing scenarios or under advanced memory management constraints, such as transactional memories.
- Advanced Combinatorial Test Design (CTD) technology that dramatically reduces the number of tests required to achieve a desired level of parameter interaction coverage over the test space of the program or system under test.
- Analytics framework to provide insights on Big Data collected during the verification/testing process, enabling better decision making in the verification process.
Our primary clients within IBM are IBM Hybrid Cloud, IBM Systems and Global Business Services. Many of our tools which are used internally are generic and are used by external clients as well.
The technologies developed in our department have received multiple IBM awards. Our overall contribution to IBM’s hardware development was awarded an IBM Research Extraordinary Accomplishment, the highest rank for technical accomplishment awarded by IBM Research. Our CTD technology was awarded an IBM Corporate Award, the highest award granted by the IBM corporate.
Raviv Gal,
Manager, Hybrid Cloud Quality Technologies (HCQT),
IBM Research - Haifa
Activities
Publications
| Title | Authors | Conference/Journal | Year | Area |
|---|---|---|---|---|
| CrawLabel: Computing Natural-Language Labels for UI Test Cases | Yu Liu, Rahulkrishna Yandrapally, Anup Kalia, Saurabh Sinha, Rachel Tzoref-Brill, Ali Mesbah | ACM/IEEE International Conference on Automation of Software Test (AST) | 2022 | |
| TACKLETEST: A Tool for Amplifying Test Generation via Type-Based Combinatorial Coverage | Rachel Tzoref-Brill, Saurabh Sinha, Antonio Abu Nassar, Victoria Goldin, Haim Kermany | IEEE International Conference on Software Testing, Verification and Validation (ICST) | 2022 | |
| Automatic scalable system for the coverage-directed generation (CDG) problem | R. Gal, E. Haber, W. Ibraheem, B. I. Z. Nevo, and A. Ziv | DATE (Proceedings) | 2021 | |
| Risk Analysis Based On Design Version Control Data | Raviv Gal, Gil Shurek, Giora Simchoni, Avi Ziv | MLCAD 2019 | 2019 | |
| The Verification Cockpit — A One-Stop Shop for Your Verification Data | Alia Shah Eugene Rotter Divya Joshi Raviv Gal Avi Ziv | DVCon 2020 | 2020 | |
| Governance and Regulations Implications on Machine Learning | Sima Nadler, Orna Raz, and Marcel Zalmanovici | CSCML’19 | 2019 | |
| Defending via strategic ML selection | Eitan Farchi, Onn Shehory, Guy Barash | EDSMLS’19 | 2019 | |
| Optimizing hierarchical classification with adaptive nodes collapse | Sujan Perera, Orna Raz, Ramani Routray, Shenghua Bao, Marcel Zalmanovici | EDSMLS’19 | 2019 | |
| Automatically detecting data drift in machine learning classifiers | Raz, O., Zalmanovici, M., Zlotnick, A. and Farchi, E. | EDSMLS’19 | 2019 | |
| Bridging the gap between ML solutions and their business requirements using feature interactions | Guy Barash, Eitan Farchi, Ilan Jayaraman, Orna Raz, Rachel Tzoref-Brill, Marcel Zalmanovici | ESEC/FSE 2019 | 2019 | |
| Machine Learning Model Drift Detection Via Weak Data Slices | Orna Raz, Samuel Ackerman, Parijat Dube, Eitan Farchi, Marcel Zalmanovici | ICSE'21 -- DeepTest | 2021 | |
| FreaAI: Automated extraction of data slices to test machine learning models | Samuel Ackerman, Orna Raz, Marcel Zalmanovici | EDSMLS’20 | 2020 | |
| Post-Silicon Validation of the IBM POWER8 Processor | Kolan T., Mendelson H., Nahir A., Sokhin V. | Mishra P., Farahmandi F. (eds) Post-Silicon Validation and Debug. Springer, Cham | 2019 | post_silicon |
| k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms | Alexander Ivrii, Ziv Nevo, Jason Baumgartner | Formal Methods in Computer-Aided Design (FMCAD) | 2018 | Formal |
| Finding All Minimal Safe Inductive Sets | Ryan Berryhill, Alexander Ivrii, Andreas G. Veneris | Theory and Applications of Satisfiability Testing (SAT) | 2018 | Formal |
| Modify, Enhance, Select: Co-Evolution of Combinatorial Models and Test Plans | Rachel Tzoref-Brill and Shahar Maoz | Symposium on the Foundations of Software Engineering (ESEC/FSE) | 2018 | SWQ |
| Proactive and Pervasive Combinatorial Testing | Dale Blue, Orna Raz, Rachel Tzoref-Brill, Paul Wojciak, and Marcel Zalmanovici | International Conference on Software Engineering | 2018 | SWQ |
| Syntactic and Semantic Differencing for Combinatorial Models of Test Designs | Rachel Tzoref-Brill and Shahar Maoz | International Conference on Software Engineering | 2017 | SWQ |
| Cost-Effective Analysis Of Post-Silicon Functional Coverage Events | Avi Ziv, Ziv Nevo, Ronny Morad, prof. Prabhat Mishra and Farimah Farahmandi | Design, Automation and Test in Europe (DATE) | 2017 | post_silicon |
| K-Induction Without Unrolling | Arie Gurfinkel and Alexander Ivrii | Formal Methods in Computer-Aided Design (FMCAD) | 2017 | Formal |
| Learning Support Sets In Ic3 And Quip: The Good, The Bad, And The Ugly | Ryan Berryhill, Alexander Ivrii, Neil Veira and Andreas Veneris | Formal Methods in Computer-Aided Design (FMCAD) | 2017 | Formal |
| Post-Silicon Validation In The Soc Era: A Tutorial Introduction | Avi Ziv, Ronny Morad, Prof. Prabhat Mishra and Sandip Ray | IEEE Design & Test journal, June | 2017 | post_silicon |
| Solving Constraint Satisfaction Problems Containing Vectors Of Unknown Size | Erez Bilgory, Eyal Bin and Avi Ziv | Principles and Practice of Constraint Programming (CP) | 2017 | CSP |
| Template Aware Coverage -Taking Coverage Analysis To The Next Level | Avi Ziv, Michael Behm, Raviv Gal, Bryan Hickerson, Einat Kermany, Bilal Saleh | Design Automation Conference (DAC) | 2017 | |
| Coverage-Based Metrics for Cloud Adaptation | Yonit Magid, Rachel Tzoref-Brill, and Marcel Zalmanovici | International Workshop on Quality-Aware DevOps (QUDOS) | 2016 | SWQ |
| Visualization of Combinatorial Models and Test Plans | Rachel Tzoref-Brill, Paul Wojciak, and Shahar Maoz | International Conference on Automated Software Engineering (ASE) | 2016 | SWQ |
| Cluster-Based Test Suite Functional Analysis | Marcel Zalmanovici, Orna Raz and Rachel Tzoref-Brill | Symposium on the Foundations of Software Engineering (ESEC/FSE) | 2016 | SWQ |
| Constrained Sampling And Counting: Universal Hashing Meets SAT Solving | Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, Sharad Malik | AAAI Workshop | 2016 | |
| Designing Reliable Cyber-Physical Systems | Gadi Aleksandrowicz, Eli Arbel, Roderick Bloem, Timon ter Braak, Sergei Devadze, Goerschwin Fey, Maksim Jenihhin, Artur Jutman, Hans G. Kerkhoff, Robert Könighofer, Jan Malburg, Shiri Moran, Jaan Raik, Gerard Rauwerda, Heinz Riener, Franz Röck ,Konstantin Shibin, Kim Sunesen, Jinbo Wan, Yong Zhao | Forum on specification & Design Languages (FDL) | 2016 | |
| Gating Aware Error Injection | Eli Arbel, Erez Barak, Bodo Hoppe, Shlomit Koyfman, Udo Krautz, Shiri Moran | Haifa Verification Conference (HVC) | 2016 | Formal |
| Isa-Independent Post-Silicon Validation For The Address Translation Mechanisms Of Modern Microprocessors | George PAPADIMITRIOU, Athanasios CHATZIDIMITRIOU, Dimitris GIZOPOULOS, Ronny MORAD | On-Line Testing and Robust System Design (IOLTS) | 2016 | post_silicon |
| On Computing Minimal Independent Support And Its Applications To Sampling And Counting | Moshe Y. Vardi, Sharad Malik, Alexander Ivrii, Kuldeep S. Meel | Constraints - An International Journal, January | 2016 | Formal |
| Probabilistic Bug-Masking Analysis For Post-Silicon Tests In Microprocessor Verification | Doowon Lee, Tom Kolan, Arkadiy Morgenshtein, Vitali Sokhin, Ronny Morad, Avi Ziv, Valeria Bertacco | Design Automation Conference (DAC) | 2016 | post_silicon |
| Test Generation Methods For Utilization Improvement Of Hardware-Accelerated Simulation Platforms | Wisam Kadry, Dmitry Krestyashyn, Arkadiy Morgenshtein, Amir Nahir, Vitali Sokhin, Jin Sung Park, Sung-Boem Park, Wookyeong Jeong, Jae-Cheol Son | IEEE Design & Test , IEEE | 2016 | |
| The Art Of Semi-Formal Bug Hunting | Pradeep Kumar Nalla, Raj Kumar Gajavelly, Jason Baumgartner, Hari Mony, Robert Kanzelman, Alexander Ivrii | International Conference on Computer Aided Design (ICCAD) | 2016 | Formal |
| Unveiling Difficult Bugs In Address Translation Caching Arrays For Effective Post-Silicon Validation | George Papadimitriou, Dimitris Gizopoulos, Athanasios Chatzidimitriou, Tom Kolan, Anatoly Koyfman, Ronny Morad and Vitali Sokhin | International Conference on Computer Design (ICCD) | 2016 | post_silicon |
| Using Graph-Based CSP To Solve The Address Translation Problem | Merav Aharoni, Yael Ben-Haim, Shai Doron, Anatoly Koyfman, Elena Tsanko and Michael Veksler | Principles and Practice of Constraint Programming (CP) | 2016 | CSP |
| Lattice-Based Semantics for Combinatorial Model Evolution | Rachel Tzoref-Brill and Shahar Maoz | International Symposium on Automated Technology for Verification and Analysis (ATVA) | 2015 | SWQ |
| Combining Minimization and Generation for Combinatorial Testing | Itai Segall, Rachel Tzoref-Brill, and Aviad Zlotnick | International Workshop on Combinatorial Testing (IWCT) | 2015 | SWQ |
| Feedback-Driven Combinatorial Test Design and Execution | Itai Segall and Rachel Tzoref-Brill | International Systems and Storage Conference (Systor) | 2015 | SWQ |
| Comparative Study Of Test Generation Methods For Simulation Accelerators | Wisam Kadry, Dmitry Krestyashyn, Arkadiy Morgenshtein, Amir Nahir, Vitali Sokhin, Jin Sung Park, Sung{-}Boem Park, Wookyeong Jeong, Jae{-}Cheol Son | Design, Automation and Test in Europe (DATE) | 2015 | |
| Constrained Sampling And Counting - Universal Hashing Meets SAT Solving | Supratik Chakraborty, Alexander Ivrii, Moshe Y. Vardi, Sharad Malik, Dror Fried, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia | CoRR | 2015 | Formal |
| Designer-Level Verification – An Industrial Experience Story | Stephen Bergman, Gabor Bobok, Walter Kowalski, Shlomit Koyfman, Shiri Moran, Ziv Nevo, Avigail Orni, Viresh Paruthi, Wolfgang Roesner, Gil Shurek, Vasantha Vuyyuru | Design, Automation and Test in Europe (DATE) | 2015 | |
| Mining Backbone Literals In Incremental SAT - A New Kind Of Incremental Data | Vadim Ryvchin, Alexander Ivrii, Ofer Strichman | Theory and Applications of Satisfiability Testing (SAT) | 2015 | Formal |
| Pushing To The Top | Arie Gurfinkel, Alexander Ivrii | Formal Methods in Computer-Aided Design (FMCAD) . The paper received the Best Application Paper Award | 2015 | Formal |
| Rectangle Placement For Vlsi Testing | Merav Aharoni, Odellia Boni, Ari Freund, Lidor Goren, Wesam Ibraheem, Tamir Segev | Artificial Intelligence and Operations Research techniques in Constraint Programming (CPAIOR) | 2015 | CSP |
| Solutions To IBM Power8 Verification Challenges | K.-D. Schubert, J. M. Ludden, S. Ayub, J. Behrend, B. Brock, F. Copty, S. M. German, O. Hershkovitz, H. Horbach, J. R. Jackson, K. Keuerleber, J. Koesters, L. S. Leitner, G. B. Meil, C. Meissner, R. Morad, A. Nahir, V. Paruthi, R. D. Peterson, R. R. Pratt, M. Rimon, J. A. Schumann | IBM Journal of Research and Development Vol 59 | 2015 | |
| Speeding Up Mus Extraction With Preprocessing And Chunking | Valeriy Balabanov, Alexander Ivrii | Theory and Applications of Satisfiability Testing (SAT) | 2015 | Formal |
| The Verifiation Cockpit - Creating The Dream Playground For Data Analytics Over The Verification Process | Moab Arar, Michael Behm, Odellia Boni, Raviv Gal, Alex Goldin, Maxim Ilyaev, Einat Kermany, John Reysa, Bilal Saleh, Klaus-Dieter Schubert, Gil Shurek, Avi Ziv | Haifa Verification Conference (HVC) | 2015 | |
| System Level Combinatorial Testing in Practice - The Concurrent Maintenance Case Study | Paul Wojciak and Rachel Tzoref-Brill | International Conference on Software Testing, Verification and Validation (ICST) | 2014 | SWQ |
| Combinatorial Testing with Order Requirements | Eitan Farchi, Itai Segall, Rachel Tzoref-Brill, Aviad Zlotnick | International Workshop on Combinatorial Testing (IWCT) | 2014 | SWQ |
| Archived: Architectural Checking Via Event Digests For High Performance Validation | Chang-Hong Hsu, Debapriya Chatterjee, Ronny Morad, Raviv Gal, Valeria Bertacco | Design, Automation and Test in Europe (DATE) | 2014 | |
| Automated Detection And Verification Of Parity-Protected Memory Elements | Eli Arbel, Shlomit Koyfman, Prabhakar Kudva, Shiri Moran | International Conference on Computer Aided Design (ICCAD) | 2014 | Formal |
| Delivering Services With Excellence In Analytics Across The Enterprise: How IBM Realizes Business Value From Big Data And Analytic (Book Chapter) | Brenda L. Dietrich, Emily C. Plachy, Maureen F. Norton | Norton, IBM Press, . | 2014 | CSP |
| Effective Post-Silicon Failure Localization Using Dynamic Program Slicing | Ophir Friedler, Wisam Kadry, Arkadiy Morgenshtein, Amir Nahir, Vitali Sokhin | Design, Automation and Test in Europe (DATE) | 2014 | post_silicon |
| Facilitating Timing Debug By Logic Path Correspondence | Oshri Adler; Eli Arbel; Ilia Averbouch; Ilan Beer; Inna Grijnevitch | Design, Automation and Test in Europe (DATE) | 2014 | |
| Future Soc Verification Methodology: Uvm Evolution Or Revolution? | Rolf Drechsler, Christophe Chevallaz, Franco Fummi, Alan J. Hu, Ronny Morad, Frank Schirrmeister, Alex Goryachev | Design, Automation and Test in Europe (DATE) | 2014 | |
| Generating Modulo-2 Linear Invariants For Hardware Model Checking | Gadi Aleksandrowicz, Oded Margalit, Alexander Ivrii, Dan Rasin | Haifa Verification Conference (HVC) | 2014 | Formal |
| Safety And Liveness, Weakness And Strength, And The Underlying Topological Relations | John Havlicek, Cindy Eisner, Dana Fisman | ACM Trans. Comput. Log. | 2014 | Formal |
| Small Inductive Safe Invariants | Anton Belov, Arie Gurfinkel, Alexander Ivrii | Formal Methods in Computer-Aided Design (FMCAD) | 2014 | Formal |
| The Computational Complexity Of Structure-Based Causality | Hana Chockler, Gadi Aleksandrowicz, Joseph Y. Halpern, Alexander Ivrii | CoRR | 2014 | Formal |
| Using A High-Level Test Generation Expert System For Testing In-Car Networks | Adir Allon, Goryachev Alex, Greenberg Lev, Salman Tamer | Design Automation Conference (DAC) | 2014 | |
| Verification Of Transactional Memory In Power8 | Adir Allon, Goodman Dave, Hershcovich Daniel, Hershkovitz Oz, Hickerson Bryan, Holtz Karen, Kadry Wisam, Koyfman Anatoly, Ludden John, Meissner Charles, others | Design Automation Conference (DAC) | 2014 | |
| Interaction-Based Test-Suite Minimization | Dale Blue, Itai Segall, Rachel Tzoref-Brill, Aviad Zlotnick | International Conference on Software Engineering (ICSE) | 2013 | SWQ |
| Using Projections to Debug Large Combinatorial Models | Eitan Farchi, Itai Segall, Rachel Tzoref-Brill | International Workshop on Combinatorial Testing (IWCT) | 2013 | SWQ |
| Generalized Counterexamples To Liveness Properties | Gadi Aleksandrowicz, Alexander Ivrii, Jason Baumgartner, Ziv Nevo | Formal Methods in Computer-Aided Design (FMCAD) | 2013 | Formal |
| Hybrid Checking For Microarchitectural Validation Of Microprocessor Designs On Acceleration Platforms | Debapriya Chatterjee, Biruk Mammo, Doowon Lee, Raviv Gal, Ronny Morad, Amir Nahir, Avi Ziv, Valeria Bertacco | Computer Aided Design (ICCAD) | 2013 | |
| Improving Post-Silicon Validation Efficiency By Using Pre-Generated Data | Amir Nahir, Wisam Kadry, Anatoly Koyfman, Dmitry Krestyashyn, Shimon Landa and Vitali Sokhin, | Haifa Verification Conference (HVC) | 2013 | post_silicon |
| Slam: Slice And Merge – Effective Test Generation For Large Systems | Tali Rabetti, Ronny Morad, Alex Goryachev, Wisam Kadry and Richard D. Peterson, | Haifa Verification Conference (HVC) | 2013 | |
| Using Cross-Entropy For Satisfiability | Hana Chockler, Arie Matsliah, Simone Fulvio Rollini, Alexander Ivrii, Natasha Sharygina | Annual ACM Symposium on Applied Computing (SAC) | 2013 | Formal |
| Common Patterns in Combinatorial Models | Itai Segall, Rachel Tzoref-Brill, Aviad Zlotnick | International Workshop on Combinatorial Testing | 2012 | SWQ |
| Simplified Modeling of Combinatorial Test Spaces | Itai Segall, Rachel Tzoref-Brill, Aviad Zlotnick | International Workshop on Combinatorial Testing | 2012 | SWQ |
| Interactive Refinement of Combinatorial Test Plans | Itai Segall, Rachel Tzoref-Brill | International Conference on Software Engineering (ICSE) | 2012 | SWQ |
| A New Test-Generation Methodology For System-Level Verification Of Production Processes | Adir, Allon and Goryachev, Alex and Greenberg, Lev and Salman, Tamer and Shurek, Gil | Haifa Verification Conference (HVC) | 2012 | |
| A Novel Approach For Implementing Microarchitectural Verification Plans In Processor Designs | Yoav Katz, Michal Rimon, Avi Ziv | Haifa Verification Conference (HVC) | 2012 | |
| Applying Constraint Programming To Incorporate Engineering Methodologies Into The Design Process Of Complex Systems | O. Boni, F. Fournier, N. Mashkif, Y. Naveh, A. Sela, U. Shani, Z. Lando, A. Modai | Innovative Applications of Artificial Intelligence (IAAI) | 2012 | CSP |
| Approximating Checkers For Simulation Acceleration | Biruk Mammo, Debapriya Chatterjee, Dmitry Pidan, Amir Nahir, Avi Ziv, Ronny Morad, Valeria Bertacco | Design, Automation and Test in Europe (DATE) | 2012 | |
| Augmenting Clause Learning With Implied Literals - (Poster Presentation) | Arie Matsliah, Ashish Sabharwal, Horst Samulowitz | Theory and Applications of Satisfiability Testing (SAT) | 2012 | Formal |
| Checking Architectural Outputs Instruction-By-Instruction On Acceleration Platforms | Debapriya Chatterjee, Anatoly Koyfman, Ronny Morad, Avi Ziv, Valeria Bertacco | Design Automation Conference (DAC) | 2012 | |
| Complete And Effective Robustness Checking By Means Of Interpolation | Stefan Frehse; Görschwin Fey; Eli Arbel; Karen Yorav; Rolf Drechsler | Formal Methods in Computer-Aided Design (FMCAD) | 2012 | |
| Computing Interpolants Without Proofs | Hana Chockler, Arie Matsliah, Alexander Ivrii | Haifa Verification Conference (HVC) | 2012 | Formal |
| Computing Mutation Coverage In Interpolation-Based Model Checking | Hana Chockler, Daniel Kroening, Mitra Purandare | IEEE Trans. on CAD of Integrated Circuits and Systems | 2012 | Formal |
| Concurrent Generation Of Concurrent Programs For Post-Silicon Validation | Allon Adir, Amir Nahir, Avi Ziv | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems: Volume 31 Issue 8, August | 2012 | |
| Generating Instruction Streams Using Abstract CSP | Yoav Katz, Michal Rimon, Avi Ziv | Design, Automation and Test in Europe (DATE) | 2012 | CSP |
| Ic3-Guided Abstraction | Hari Mony, Arie Matsliah, Alexander Ivrii, Jason Baumgartner | Formal Methods in Computer-Aided Design (FMCAD) | 2012 | Formal |
| Nutab-Backspace: Rewriting To Normalize Non-Determinism In Post-Silicon Debug Traces | F. De Paula, A. Hu, A. Nahir | Computer Aided Verification (CAV) | 2012 | |
| On Efficient Computation Of Variable Muses | Alexander Ivrii, Anton Belov, Arie Matsliah, Joao Marques-Silva | Theory and Applications of Satisfiability Testing (SAT) | 2012 | Formal |
| Perfect Hashing And Cnf Encodings Of Cardinality Constraints | Y. Ben-Haim, A. Ivrii, O. Margalit and A. Matsliah | Theory and Applications of Satisfiability Testing (SAT) | 2012 | Formal, csp, SAT |
| Relating Proof Complexity Measures And Practical Hardness Of SAT | Matti Järvisalo, Arie Matsliah, Jakob Nordström, Stanislav Živný | Principles and Practice of Constraint Programming (CP) | 2012 | Formal |
| Verification Of Software Changes With Explisat | Hana Chockler, Sitvanit Ruah | Workshop on Hot Topics in Software Upgrades (HotSWUp) | 2012 | Formal |
| Using Binary Decision Diagrams for Combinatorial Test Design | Itai Segall, Rachel Tzoref-Brill, and Eitan Farchi | International Symposium on Software Testing and Analysis (ISSTA), | 2011 | SWQ |
| A Probabilistic Analysis Of Coverage Methods | Laurent Fournier, Avi Ziv, Ekaterina Kutsy, Ofer Strichman | ACM Transactions on Design Automation of Electrolic Systems (TODAES) | 2011 | |
| A Unified Methodology For Pre-Silicon Verification And Post-Silicon Validation | A Adir, S Copty, S Landa, A Nahir, G Shurek, A Ziv, C Meissner, J Schumann | Design Automation and Test in Europe (DATE) | 2011 | post_silicon |
| Automatic Boosting Of Cross-Product Coverage Using Bayesian Networks | D Baras, S. Fine, L. Fournier, D. Geiger, A. Ziv | International Journal on Software Tools for Technology Transfer (STTT) | 2011 | |
| Dynamic Test Data Generation For Data Intensive Application | Tamer Salman, Ronen Levy, and Allon Adir | Haifa Verification Conference (HVC) | 2011 | |
| Facing The Challenge Of New Design Features An Effective Verification Approach | Wisam Kadry, Ronny Morad, Eli Almog, Alex Goryachev, Christopher Krygowski | Design Automation Conference (DAC) | 2011 | |
| Floorplanning Challenges In Early Chip Planning | Jeonghee Shin, John A Darringer, Guojie Luo, Merav Aharoni, Alexey Y Lvov, G Nam, Michael B Healy | SOC Conference (SOCC) | 2011 | CSP |
| Functional Verification Of The IBM Power7 Microprocessor And Power7 Multiprocessor Systems | 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 | IBM Journal of Research and Development Vol 55 | 2011 | |
| Guaranteeing High Availability Goals For Virtual Machine Placement | E. Bin, O. Biran, O. Boni, E. Hadad, E. K. Kolodner, Y. Moatti, D. H. Lorenz | Distributed Computing Systems (ICDCS) | 2011 | CSP |
| Incremental Formal Verification Of Hardware | Hana Chockler, Shiri Moran, Arie Matsliah, Alexander Ivrii, Ziv Nevo | Formal Methods in Computer-Aided Design (FMCAD) | 2011 | Formal |
| Injecting Floating-Point Testing Knowledge Into Test Generators | Elena Guralnik, Anatoly Koyfman, Emanuel Gofman, and Merav Aharoni | Hardware and Software Verification and Testing, Seventh International Haifa Verification Conference (HVC), | 2011 | |
| Learning Microarchitectural Behaviors To Improve Stimuli Generation Quality | Yoav Katz, Michal Rimon, Gai Shaked, Avi Ziv | Design Automation Conference (DAC) | 2011 | |
| Leveraging Pre-Silicon Verification Resources For The Post-Silicon Validation Of The IBM Power7 Processor | Adir, Allon and Nahir, Amir and Shurek, Gil and Ziv, Avi and Meissner, Charles and Schumann, John | Design Automation Conference (DAC) | 2011 | post_silicon |
| Reducing The Size Of Resolution Proofs In Linear Time | Omer Bar-Ilan, Ohad Shacham, Shlomo Hoory, Oded Fuhrmann, Ofer Strichman | International Journal on Software Tools for Technology Transfer (STTT) June | 2011 | Formal |
| Reverse Coverage Analysis | Ariel Birnbaum, Laurent Fournier, Avi Ziv, and Steve Mittermaier | Haifa Verification Conference (HVC) | 2011 | |
| Simulation-Based Verification Of Floating-Point Division | Elena Guralnik, Merav Aharoni, Ariel J. Birnbaum, Anatoly Koyfman | IEEE Trans Computers 60(2) 176-188 | 2011 | |
| Stimuli Generation For Functional Hardware Verification With Constraint Programming (Book Chapter) | Allon Adir and Yehuda Naveh | Hybrid Optimization - The Ten Years of CPAIOR, by Pascal Van Hentenryck and Michela Milano, Springer, | 2011 | CSP |
| Tab-Backspace Unlimited-Length Trace Buffers With Zero Additional On-Chip Overheads | Alan Hu, Flavio M De-Paula, Avigail Orni, Ziv Nevo, and Amir Nahir | Design Automation Conference (DAC) | 2011 | |
| Threadmill A Post-Silicon Exerciser For Multi-Threaded Processors | Allon Adir, Maxim Golubev, Shimon Landa, Amir Nahir, Gil Shurek, Vitali Sokhin, Avi Ziv | Design Automation Conference (DAC) | 2011 | post_silicon |
| Improving throughput via slowdowns | Maayan Goldstein, Onn Shehory, Rachel Tzoref-Brill, and Shmuel Ur | International Conference on Software Engineering (ICSE) | 2010 | SWQ |
| Advances In Simultaneous Multithreading Testcase Generation Methods | John Ludden, Michal Rimon, Bryan Hickerson, Allon Adir | Haifa Verification Conference (HVC), | 2010 | |
| An Ontology And Constraint Based Approach To Cache Preloading | Rajiv Bhatia, Eyal Bin, Eitan Marcus, Gil Shurek | High-Level Design Validation and Test Workshop (HLDVT) | 2010 | |
| Applying Constraint Programming To Identification And Assignment Of Service Professionals | S. Asaf, H. Eran, Y. Richter, D. P Connors, D. L. Gresh, J. Ortega, M. J. Mcinnis | Principles and Practice of Constraint Programming (CP). The paper received the Best Application Paper Award | 2010 | CSP |
| Coverage In Interpolation-Based Model Checking | Hana Chockler, Daniel Kroening, Mitra Purandare | Design Automation Conference (DAC) | 2010 | Formal |
| Ontology-Based Tools In The Service Of Hardware Verification | Eyal Bin, Alaa Ghanayim, Karen Holtz, Eitan Marcus, Ronny Morad, Ofer Peled, Michal Rimon, Gil Shurek, Elena Tsanko | Software Engineering & Knowledge Engineering (SEKE) | 2010 | |
| Reaching Coverage Closure In Post-Silicon Validation | A Adir, A Nahir, A Ziv, C Meissner, J Schumann | Haifa Verification Conference (HVC) | 2010 | |
| Simulation Based Verification Of Floating Point Division | Elena Guralnik, Merav Aharoni, Ariel J. Birnbaum, Anatoly Koyfman | IEEE Transactions on Computers | 2010 | fpgen |
| The Big Deal, Applying Constraint Satisfaction Technologies Where It Makes The Difference | Y. Naveh | Theory and Applications of Satisfiability Testing (SAT) | 2010 | CSP |
| Underapproximation For Model-Checking Based On Universal Circuits | Ofer Strichman, Arie Matsliah | Inf. Comput. | 2010 | Formal |
| Variants Of LTL Query Checking | Hana Chockler, Arie Gurfinkel, Ofer Strichman | Haifa Verification Conference (HVC) | 2010 | Formal |
| A Concurrency Testing Tool and Its Plug-Ins for Dynamic Analysis and Runtime Healing | Bohuslav Krena, Zdenek Letko, Yarden Nir-Buchbinder, Rachel Tzoref-Brill, Shmuel Ur, and Tomas Vojnar | International Workshop on Runtime Verification (RV) | 2009 | SWQ |
| Forcing small models of conditions on program interleaving for detection of concurrent bugs | Ehud Trainin, Yarden Nir-Buchbinder, Rachel Tzoref-Brill, Aviad Zlotnick, Shmuel Ur, and Eitan Farchi | Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD) | 2009 | SWQ |
| Before And After Vacuity | Hana Chockler, Ofer Strichman | Formal Methods in System Design 34(1), Springer | 2009 | Formal |
| Cross-Entropy-Based Replay Of Concurrent Programs | Hana Chockler, Eitan Farchi, Benny Godlin, Sergey Novikov | Fundamental Approaches to Software Engineering (FASE) | 2009 | Formal |
| Explaining Counterexamples Using Causality | Shoham Ben-David, Hana Chockler, Avigail Orni, Ilan Beer, Richard J. Trefler | Computer Aided Verification (CAV) | 2009 | Formal |
| Functional Verification Of Power Gated Designs By Compositional Reasoning | Cindy Eisner, Amir Nahir, Karen Yorav | Formal Methods in System Design | 2009 | Formal |
| Implementation Specific Verification Of Divide And Square Root Instructions | Elena Guralnik, Ariel J. Birnbaum, Anatoly Koyfman, Avi Kaplan | IEEE Symposium on Computer Arithmetic (ARITH) | 2009 | fpgen |
| Multicore Power Management: Ensuring Robustness Via Early-Stage Formal Verification | Anita Lungu, Pradip Bose, Daniel J Sorin, Steven German, Geert Janssen | Formal Methods and Models for Co-Design (MEMOCODE), | 2009 | |
| On Extending Bounded Proofs To Inductive Proofs | Oded Fuhrmann, Shlomo Hoory | Computer Aided Verification (CAV) | 2009 | Formal |
| Pin Assignment Using Stochastic Local Search Constraint Programming | B. Dubrov, H. Eran, A. Freund, E. F. Mark, S. Ramji, and T. A. Schell, | Priniciples and Practice of Constraint Programming (CP) | 2009 | CSP |
| SAT-Based Synthesis Of Clock Gating Functions Using 3-Valued Abstraction | Karen Yorav, Oleg Rokhlenko, Eli Arbel | Formal Methods in Computer-Aided Design (FMCAD) | 2009 | Formal |
| Scalable Conditional Equivalence Checking - An Automated Invariant-Generation Based Approach | Hari Mony, Michael L. Case, Jun Sawada, Jason Baumgartner, Karen Yorav | Formal Methods in Computer-Aided Design (FMCAD) | 2009 | Formal |
| User-Friendly Model Checking: Automatically Configuring Algorithms With Rulebase/Pe | Z Nevo | Haifa Verification Conference (HVC) | 2009 | |
| Using Bayesian Networks And Virtual Coverage To Hit Hard-To-Reach Events | Shai Fine, Laurent Fournier, Avi Ziv | International Journal on Software Tools for Technology Transfer (STTT) 11(4) 291-305 | 2009 | |
| Deadlocks: From Exhibiting to Healing | Yarden Nir-Buchbinder, Rachel Tzoref, and Shmuel Ur | International Workshop on Runtime Verification (RV) | 2008 | SWQ |
| Automatic Debugging of Concurrent Programs through Active Sampling of Low Dimensional Random Projections | Elad Yom-Tov, Rachel Tzoref, Shmuel Ur, and Shlomo Hoory | International Conference on Automated Software Engineering (ASE) | 2008 | SWQ |
| Experience with a concurrency bugs benchmark | Yaniv Eytani, Rachel Tzoref, Shmuel Ur | Software Testing Verification and Validation Workshop (ICSTW) | 2008 | SWQ |
| A Probabilistic Alternative To Regression Suites | Shady Copty, Shai Fine, Shmuel Ur, Elad Yom-Tov, Avi Ziv | Theoretical Computer Science 404(3), 219--234, Elsevier | 2008 | |
| Augmenting A Regular Expression-Based Temporal Logic With Local Variables | Cindy Eisner, Dana Fisman | Formal Methods in Computer-Aided Design (FMCAD) | 2008 | Formal |
| Automatic Boosting Of Cross-Product Coverage Using Bayesian Networks | Dorit Baras, Laurent Fournier, Avi Ziv | Haifa Verification Conference (HVC) | 2008 | |
| Beyond Vacuity: Towards The Strongest Passing Formula | Hana Chockler, Ofer Strichman and Arie Gurfinkel | Formal Methods in Computer-Aided Design (FMCAD) | 2008 | Formal |
| Efficient Automatic STE Refinement Using Responsibility | Hana Chockler, Orna Grumberg, Avi Yadgar | Tools and algorithms for the construction and analysis of systems (TACAS) | 2008 | Formal |
| Embedding Finite Automata Within Regular Expressions | Shoham Ben-David, Dana Fisman, Sitvanit Ruah | Theor. Comput. Sc | 2008 | Formal |
| Functional Verification Of Power Gated Designs By Compositional Reasoning | Cindy Eisner, Amir Nahir, Karen Yorav | Computer Aided Verification (CAV) | 2008 | |
| IBM System Z Functional And Performance Verification Using X-Gen | Torsten Schober, Bodo Hoppe, Shimon Landa, Ronny Morad | High-Level Design Validation and Test Workshop (HLDVT) | 2008 | |
| Linear-Time Reductions Of Resolution Proofs | Omer Bar-Ilan, Ohad Shacham, Shlomo Hoory, Oded Fuhrmann, Ofer Strichman | Haifa Verification Conference (HVC) | 2008 | Formal |
| Policy Validation For System Automation - A Case Study | Cindy Eisner, Emmanuel Zarpas, Sivan Tal | Policies for Distributed Systems and Networks, , pp. 46--53 | 2008 | Formal |
| Structural Contradictions | Cindy Eisner and Dana Fisman | Haifa Verification Conference (HVC) | 2008 | Formal |
| User-Friendly Model Checking - Automatically Configuring Algorithms With Rulebase/Pe | Ziv Nevo | Haifa Verification Conference (HVC) | 2008 | Formal |
| What Causes A System To Satisfy A Specification ? | Hana Chockler, Joseph Y. Halpern, Orna Kupferman | ACM Trans. Comput. Log. | 2008 | Formal |
| Healing data races on-the-fly | Bohuslav Krena, Zdenek Letko, Rachel Tzoref, Shmuel Ur, and Tomas Vojnar | Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD) | 2007 | SWQ |
| Instrumenting where it hurts: an automatic concurrent debugging technique | Rachel Tzoref, Shmuel Ur, and Elad Yom-Tov | International Symposium on Software Testing and Analysis (ISSTA) | 2007 | SWQ |
| A Framework For The Validation Of Processor Architecture Compliance | Allon Adir, Sigal Asaf, Laurent Fournier, Itai Jaeger, Ofer Peled | Design Automation Conference (DAC) | 2007 | |
| A Methodology For Formal Design Of Hardware Control With Application To Cache Coherence Protocols | Cindy Eisner | RV | 2007 | Formal |
| Constraint-Based Random Stimuli Generation For Hardware Verification | Yehuda Naveh, Michal Rimon, Itai Jaeger, Yoav Katz, Michael Vinov, Eitan Marcus, Gil Shurek | AI Magazine 28(3), pages 13-30 | 2007 | |
| Decimal Floating-Point In Z9: An Implementation And Testing Perspective | A.Y. Duale, M.H.Decker, H.-G.Zipperer, Merav Aharoni, T.J.Bohizic | IBM Journal of Research and Development 51(1/2)217-228 | 2007 | fpgen |
| Easier And More Informative Vacuity Checks | Hana Chockler, Ofer Strichman | Formal Methods and Models for Codesign (MEMOCODE) | 2007 | Formal |
| Explisat: Guiding SAT-Based Software Verification With Explicit States | S Barner, C Eisner, Z Glazberg, D Kroening, I Rabinovitz | Haifa Verification Conference (HVC) | 2007 | |
| Intelligent Interleaving Of Scenarios A Novel Approach To System Level Test Generation | Shady Copty, Itai Jaeger, Yoav Katz, Michael Vinov | Design Automation Conference (DAC) | 2007 | |
| On The Characterization Of Until As A Fixed Point Under Clocked Semantics | Dana Fisman | Haifa Verification Conference (HVC) | 2007 | Formal |
| On-The-Fly Resolve Trace Minimization | Ohad Shacham, Karen Yorav | Design Automation Conference (DAC) | 2007 | Formal |
| Optimatch: Applying Constraint Programming To Workforce Management Of Highly-Skilled Employees | Y. Richter, Y. Naveh, D. L. Gresh, and D. P. Connors | International Journal of Services Operations and Informatics (IJSOI) | 2007 | CSP |
| Preprocessing Expression-Based Constraint Satisfaction Problems For Stochastic Local Search | S. Sabato and Y. Naveh | Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR) | 2007 | CSP |
| Solving Constraints On The Intermediate Result Of Decimal Floating Point Operations | Merav Aharoni, Ron Maharik, Abraham Ziv | IEEE Symposium on Computer Arithmetic (ARITH) | 2007 | fpgen |
| Using Virtual Coverage To Hit Hard-To-Reach Events | Laurent Fournier, Avi Ziv | Haifa Verification Conference (HVC) | 2007 | |
| Workforce Optimization: Identification And Assignment Of Professional Workers Using Constraint Programming | Y. Naveh, Y. Richter, Y. Altshuler, D. Gresh, and D. Connors | IBM J. R&D | 2007 | CSP |
| A Practical Introduction To PSL | Cindy Eisner, Dana Fisman | Series on Integrated Circuits and Systems | 2006 | Formal |
| Adaptive Application Of SAT Solving Techniques | Ohad Shacham, Karen Yorav | Electr. Notes Theor. Comput. Sci. | 2006 | Formal |
| Addressing Test Generation Challenges For Configurable Processor Verification | M Rimon, Y Lichtenstein, A Adir, I Jaeger, M Vinov, S Johnson, D Jani | High-Level Design Validation and Test Workshop (HLDVT) | 2006 | gpro |
| Advanced Analysis Techniques For Cross-Product Coverage | H Azatchi, L Fournier, E Marcus, S Ur, A Ziv, K Zohar | IEEE Transactions on Computers | 2006 | |
| Automatic Verification Of Fault-Tolerant Register Emulations | PC Attie, H Chockler | Electronic Notes in Theoretical Computer Science (ENTCS) | 2006 | |
| Behavioral Compatibility Without State Explosion: Design And Verification Of A Component-Based Elevator Control System | PC Attie, DH Lorenz, A Portnova, H Chockler | Component-Based Software Engineering (CBSE) | 2006 | |
| Constraint-Based Random Stimuli Generation For Hardware Verification | Yehuda Naveh, Michal Rimon, Itai Jaeger, Yoav Katz, Michael Vinov, Eitan Marcus, Gil Shurek | Innovative Applications of Artificial Intelligence Conference (IAAI), | 2006 | |
| Coverage Metrics For Formal Verification | H Chockler, O Kupferman, M Vardi | Int J Softw Tools Technol Transfer | 2006 | |
| Coverage Metrics For Temporal Logic Model Checking* | H Chockler, O Kupferman, MY Vardi | Formal Methods in System Design, | 2006 | |
| Deeptrans - Extending The Model-Based Approach To Functional Verification Of Address Translation Mechanisms | Allon Adir, Laurent Fournier, Yoav Katz, Anatoly Koyfman | High-Level Design Validation and Test Workshop (HLDVT) | 2006 | |
| Distributed Dynamic BDD Reordering | Monica Farkash, Ziv Nevo | Design Automation Conference (DAC) | 2006 | Formal |
| Explisat - Guiding SAT-Based Software Verification With Explicit States | Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening and Ishai Rabinovitch | Haifa Verification Conference (HVC) | 2006 | Formal |
| Formal Verification Of Concurrent Software: Two Case Studies | Hana Chockler, Eitan Farchi, Ziv Glazberg, Benny Godlin, Yarden Nir-Buchbinder, Ishai Rabinovitz | Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD), | 2006 | Formal |
| Generalizing Alldifferent: The Somedifferent Constraint | Y. Richter, A. Freund, and Y. Naveh | International Conference on Principles and Practice of Constraint Programming (CP) | 2006 | CSP |
| Harnessing Machine Learning To Improve The Success Rate Of Stimuli Generation | Shai Fine, Ari Freund, Itai Jaeger, Yishay Mansour, Yehuda Naveh, Avi Ziv | IEEE Trans Computers 55(11) 1344-1355 | 2006 | |
| Random Stimuli Generation For Functional Hardware Verification As A CP Application - A Demo | Y. Naveh and R. Emek | Innovative Applications of Artificial Intelligence (IAAI) | 2006 | CSP |
| Scheduling-Based Test-Case Generation For Verification Of Multimedia Socs | Amir Nahir, Avi Ziv, Roy Emek, Tal Keidar, Nir Ronen | Design Automation Conference (DAC) | 2006 | |
| Supporting SAT Based BMC On Finite Path Models | Mark Ginzburg, Ohad Shacham, Yoad Lustig, Ishai Rabinovitz, Rachel Tzoref, Daniel Geist | Electr. Notes Theor. Comput. Sci. | 2006 | Formal |
| Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation | Rachel Tzoref and Orna Grumberg | Computer Aided Verification (CAV) | 2006 | Formal |
| Using Linear Programming Techniques For Scheduling-Based Random Test-Case Generation | Amir Nahir, Yossi Shiloach, Avi Ziv | Haifa Verification Conference (HVC) | 2006 | |
| A Generic Micro-Architectural Test Plan Approach For Microprocessor Verification | Allon Adir, Hezi Azatchi, Eyal Bin, Ofer Peled, Kirill Shoikhet | Design Automation Conference (DAC) | 2005 | |
| A Topological Characterization Of Weakness | Cindy Eisner, Dana Fisman, John Havlicek | Principles of distributed computing (PODC) | 2005 | Formal |
| Advanced Analysis Techniques For Cross-Product Coverage | Hezi Azatchi, Laurent Fournier, Avi Ziv, Keren Zohar | High-Level Design Validation and Test Workshop (HLDVT) | 2005 | |
| Assumption-Based Distribution Of CTL Model Checking | L Brim, K Yorav, J dkov | Int J Softw Tools Technol Transfer | 2005 | |
| Assumption-Based Pruning In Conditional CSP | F. Geller and M. Veksler | in van Beek, P., ed., CP | 2005 | CSP |
| Benchmarking SAT Solvers For Bounded Model Checking | Emmanuel Zarpas | Theory and Applications of Satisfiability Testing (SAT) | 2005 | Formal |
| Combining System Level Modeling With Assertion Based Verification | Anat Dahan, Daniel Geist, Leonid Gluhovsky, Dmitry Pidan, Gil Shapir, Yaron Wolfsthal | International Symposium on Quality Electronic Design (ISQED) | 2005 | Formal |
| Formal Verification - Is It Real Enough? | Yaron Wolfsthal, Rebecca M. Gott | Design Automation Conference (DAC) | 2005 | Formal |
| Harnessing Machine Learning To Improve The Success Rate Of Stimuli Generation | Shai Fine, Ari Freund, Itai Jaeger, Yehuda Naveh, Avi Ziv, Yishay Mansour | High-Level Design Validation and Test Workshop (HLDVT) | 2005 | |
| Path-Based System Level Stimuli Generation | Shady Copty, Itai Jaeger, Yoav Katz | Haifa Verification Conference (HVC) | 2005 | |
| Random Stimuli Generation For Functional Hardware Verification As A CP Application | Yehuda Naveh, Roy Emek | Principles and Practice of Constraint Programming (CP) | 2005 | |
| SATabs: SAT-Based Predicate Abstraction For Ansi-C | E Clarke, D Kroening, N Sharygina, K Yorav | Tools and Algorithms for the Construction and Analysis of Systems (TACAS) | 2005 | |
| Solving Constraints On The Invisible Bits Of The Intermediate Result For Floating-Point Verification | Merav Aharoni, Sigal Asaf, Ron Maharik, Ilan Nehama, Ilya Nikulshin, Abraham Ziv | Proceedings of the IEEE Symposium on Computer Arithmetic (ARITH) | 2005 | fpgen |
| Stochastic Solver For Constraint Satisfaction Problems With Learning Of High-Level Characteristics Of The Problem Topography | Y. Naveh | Conference on Principles and Practice of Constraint Programming (CP) | 2005 | CSP |
| Temporal Modalities For Concisely Capturing Timing Diagrams | H Chockler, K Fisler | Correct Hardware Design and Verification Methods (CHARME) | 2005 | |
| The Safety Simple Subset | Shoham Ben-David, Dana Fisman and Sitvanit Ruah | Haifa Verification Conference (HVC) | 2005 | Formal |
| VLIW: A Case Study Of Parallelism Verification | Allon Adir, Yaron Arbetman, Bella Dubrov, Yossi Lichtenstein, Michal Rimon, Michael Vinov, Massimo A. Calligaro, Andrew Cofler, Gabriel Duffy | Design Automation Conference (DAC) | 2005 | gpro |
| Wolf- Bug Hunter For Concurrent Software Using Formal Methods | Sharon Barner, Ishai Rabinovitch and Ziv Glazberg | Computer Aided Verification (CAV) | 2005 | Formal |
| omega-Regular Languages Are Testable With A Constant Number Of Queries | H Chockler, O Kupferman | Theoretical Computer Science, - Springer | 2004 | |
| A Lower Bound For Testing Juntas | Hana Chockler, Dan Gutfreund | Inf. Process. Lett. 90(6), 301--305 | 2004 | |
| Deeptrans - Extending The Model-Based Approach To Functional Verification Of Address Translation Mechanisms | Allon Adir, Roy Emek, Yoav Katz, Anatoly Koyfman | MTV ?? | 2004 | gpro |
| Defining Coverage Views To Improve Functional Coverage Analysis | Sigal Asaf, Eitan Marcus, Avi Ziv | Design Automation Conference (DAC) | 2004 | coverage |
| Efficient Verification Of Sequential And Concurrent C Programs | Clarke, A Groce, J Ouaknine, O Strichman, K Yorav | Formal Methods in System Design | 2004 | |
| Efficiently Verifiable Suficient Conditions For Deadlockfreedom Of Large Concurrent Programs | PC Attie, H Chockler | Technical report, Northeastern University, Boston, MA | 2004 | |
| Enhancing The Efficiency Of Bayesian Network Based Coverage Directed Test Generation | Marcus Braun, Shai Fine, Avi Ziv | High-Level Design Validation and Test Workshop (HLDVT) | 2004 | coverage |
| Genesys-Pro: Innovations In Test Program Generation For Functional Processor Verification | Allon Adir, Eli Almog, Laurent Fournier, Eitan Marcus, Michal Rimon, Michael Vinov, Avi Ziv | IEEE Design & Test of Computers (DT) | 2004 | gpro |
| Industrial Experience With Test Generation Languages For Processor Verification | Michael L. Behm, John M. Ludden, Yossi Lichtenstein, Michal Rimon, Michael Vinov | Design Automation Conference (DAC) | 2004 | gpro |
| Probabilistic Alternative Regression Suites | Shady Copty, Shai Fine, Shmuel Ur, Avi Ziv | International Symposium on Leveraging Applications of Formal Methods (ISoLA), | 2004 | |
| Probabilistic Regression Suites For Functional Verification | Shai Fine, Shmuel Ur, Avi Ziv | Design Automation Conference (DAC) | 2004 | |
| Quality Improvement Methods For System-Level Stimuli Generation | Roy Emek, Itai Jaeger, Yoav Katz, Yehuda Naveh | International Conference on Computer Design (ICCD) | 2004 | |
| Simple Yet Efficient Improvements Of SAT Based Bounded Model Checking | Emmanuel Zarpas | Formal Methods in Computer-Aided Design (FMCAD) | 2004 | Formal |
| Static Analysis For State-Space Reductions Preserving Temporal Logics | K Yorav, O Grumberg | Formal Methods in System Design | 2004 | |
| Stimuli Generation With Late Binding Of Values | Avi Ziv | Design Automation and Test in Europe (DATE) | 2004 | |
| Stochastic Solver For Constraint Satisfaction Problems With Learning Of High-Level Characteristics Of The Problem Topography | Y. Naveh | Local Search Techniques in Constraint Satisfaction (LSCS-04) | 2004 | CSP |
| An Optimized Symbolic Bounded Model Checking Engine | Ilan Beer, Eli Berger, Rachel Tzoref, Mark Matusevich | Correct Hardware Design and Verification Methods (CHARME) | 2003 | Formal |
| Coverage Directed Test Generation For Functional Verification Using Bayesian Networks | Shai Fine, Avi Ziv | Design Automation Conference (DAC) | 2003 | |
| Cross-Product Functional Coverage Measurement With Temporal Properties-Based Assertions | Avi Ziv | Design Automation and Test in Europe Conference (DATE) | 2003 | |
| Deeptrans - A Model-Based Approach To Functional Verification Of Address Translation Mechanisms | Allon Adir, Roy Emek, Yoav Katz, Anatoly Koyfman | Microprocessor Test and Verification (MTV) | 2003 | gpro |
| Enhancing The Control And Efficiency Of The Covering Process | Shai Fine, Avi Ziv | High-Level Design Validation and Test Workshop (HLDVT) | 2003 | |
| FPgen - A Test Generation Framework For Datapath Floating-Point Verification | Merav Aharoni, Sigal Asaf, Laurent Fournier, Anatoly Koifman, Raviv Nagel | High-Level Design Validation and Test Workshop (HLDVT) | 2003 | fpgen |
| Functional Verification Environment For Object-Oriented Hardware Designs | Avi Ziv | Forum on Design Languages (FDL), | 2003 | |
| Information-Flow Models For Shared Memory With An Application To The Powerpc Architecture | Allon Adir, Hagit Attiya, Gil Shurek | IEEE Trans Parallel Distrib Syst (TPDS) 14(5)502-515 | 2003 | gpro |
| Model Checking At IBM | Shoham Ben-David, Cindy Eisner, Yaron Wolfsthal, Daniel Geist | Formal Methods in System Design | 2003 | Formal |
| Piparazzi: A Test Program Generator For Micro-Architecture Flow Verification | Allon Adir, Eyal Bin, Ofer Peled, Avi Ziv | High-Level Design Validation and Test Workshop (HLDVT) | 2003 | |
| Reasoning With Temporal Logic On Truncated Paths | John Havlicek, Cindy Eisner, Dana Fisman, Yoad Lustig, Anthony McIsaac, David Van Campenhout | Computer Aided Verification (CAV) | 2003 | Formal |
| Scalable Distributed On-The-Fly Symbolic Model Checking | Shoham Ben-David, Orna Grumberg, Tamir Heyman, Assaf Schuster | International Journal on Software Tools for Technology Transfer (STTT) | 2003 | Formal |
| Scheduling Of Transactions For System-Level Test-Case Generation | Roy Emek, Yehuda Naveh | High-Level Design Validation and Test Workshop (HLDVT) | 2003 | |
| Searching For Counter-Examples Adaptively | Sharon Keidar, Yoav Rodeh | International Workshop in Formal Methods (IWFM) | 2003 | Formal |
| Solving Range Constraints For Binary Floating-Point Instructions | Abraham Ziv, Merav Aharoni, Sigal Asaf | IEEE Symposium on Computer Arithmetic (ARITH) | 2003 | fpgen |
| Solving The Generalized Mask Constraint For Test Generation Of Binary Floating Point Add Operation | Abraham Ziv, Laurent Fournier | Theor Comput Sci 291(2) 183-201 | 2003 | fpgen |
| The Definition Of A Temporal Clock Operator | John Havlicek, Cindy Eisner, Dana Fisman, David Van Campenhout, Anthony McIsaac | International Colloquium on Automata, Languages and Programming (ICALP) | 2003 | Formal |
| The PSL/Sugar Specification Language: A Language For All Seasons | Daniel Geist | Correct Hardware Design and Verification Methods (CHARME) | 2003 | Formal |
| Tuning The VSIDS Decision Heuristic For Bounded Model Checking | Emmanuel Zarpas, Ohad Shacham | Microprocessor Test and Verification Conference (MTV) | 2003 | Formal |
| Adaptive Test Program Generation Planning For The Unplanned | Allon Adir, Roy Emek, Eitan Marcus | High-Level Design Validation and Test Workshop (HLDVT) | 2002 | gpro |
| An Algorithmic Approach To Design Exploration | Sharon Barner, Shoham Ben-David, Anna Gringauze, Baruch Sterin, Yaron Wolfsthal | International Symposium of Formal Methods Europe (FME) | 2002 | Formal |
| An Effective And Flexible Approach To Functional Verification Of Processor Families | David Malandain, Pim Palmen, Matthew Taylor, Merav Aharoni, Yaron Arbetman | High-Level Design Validation and Test Workshop (HLDVT) | 2002 | genesys |
| Comparing Symbolic And Explicit Model Checking Of A Software System | Cindy Eisner and Doron Peled | International Symposium on Model Checking Software (SPIN) | 2002 | Formal |
| Generating Concurrent Test Programs With Collisions For Multiprocessor Verification | Allon Adir, Gil Shurek | High-Level Design Validation and Test Workshop (HLDVT) | 2002 | gpro |
| Generating Random Solutions For Constraint Satisfaction Problems | Rina Dechter, Kalev Kask, Eyal Bin, Roy Emek | National Conference on Artificial Intelligence (AAAI), | 2002 | CSP |
| Hole Analysis For Functional Coverage Data | Oded Lachish, Eitan Marcus, Shmuel Ur, Avi Ziv | Design Automation Conference (DAC) | 2002 | |
| Object-Oriented High-Level Modeling Of An Infiniband To Pci-X Bridge | Oded Lachish, Avi Ziv | System Specification & Design Languages Best of FDL'02 | 2002 | |
| Pathfinder: A Tool For Design Exploration | Shoham Ben-David, Anna Gringauze, Baruch Sterin, Yaron Wolfsthal | Computer Aided Verification (CAV) | 2002 | Formal |
| Symbolic Localization Reduction With Reconstruction Layering And Backtracking | Daniel Geist, Sharon Barner, Anna Gringauze | Computer Aided Verification (CAV) | 2002 | Formal |
| Test Generation For The Binary Floating-Point Add Operation With Mask-Mask-Mask Constraints | Abraham Ziv, Laurent Fournier | Theoretical Computer Science 291(2)183-201 | 2002 | fpgen |
| Using A Constraint Satisfaction Formulation And Solution Techniques For Random Test Program Generation | Eyal Bin, Roy Emek, Gil Shurek, Avi Ziv | IBM Systems Journal 41(3) 386-402 | 2002 | CSP |
| X-Gen: A Random Test-Case Generator For Systems And Socs | Roy Emek, Itai Jaeger, Yehuda Naveh, Gadi Bergman, Gay Aloni, Yoav Katz, Monica Farkash, Igor Dozoretz, Alex Goldin | High-Level Design Validation and Test Workshop (HLDVT) | 2002 | |
| Cost Evaluation Of Coverage Directed Test Generation For The IBM Mainframe | Gilly Nativ, Steven Mittermaier, Shmuel Ur, Avi Ziv | IEEE International Test Conference (ITC) | 2001 | |
| Coverability Analysis Using Symbolic Model Checking | Shmuel Ur, Gil Ratsaby, Yaron Wolfsthal | Correct Hardware Design and Verification Methods (CHARME) | 2001 | Formal |
| Distributed Symbolic Model Checking For µ-Calculus | Tamir Heyman | Computer Aided Verification (CAV) | 2001 | Formal |
| Efficient Detection Of Vacuity In Temporal Model Checking | Shoham Ben-David, Cindy Eisner, Ilan Beer, Yoav Rodeh | Formal Methods in System Design | 2001 | Formal |
| Improving Test Quality Through Resource Reallocation | Allon Adir, Eitan Marcus, Michal Rimon, Amir Voskoboynik | High-Level Design Validation and Test Workshop (HLDVT) | 2001 | gpro |
| Model Checking The Garbage Collection Mechanism Of SMV | Cindy Eisner | Electronic Notes in Theoretical Computer Science | 2001 | Formal |
| On The Effective Deployment Of Functional Formal Verification | Irit Shitsevalov, Iris Reuveni, Tali Yatzkar-Haham, Eran Rippel, Neta Aizenbud-Reshef, Cindy Eisner, Ilan Beer, Yaron Wolfsthal, Daniel Geist, Tamir Heyman, Yael Abarbanel-Vinov | Formal Methods in System Design | 2001 | Formal |
| The Temporal Logic Sugar | Yoav Rodeh, Shoham Ben-David, Cindy Eisner, Dana Fisman, Ilan Beer, Anna Gringauze | Computer Aided Verification (CAV) | 2001 | Formal |
| A Methodology For Formal Design Of Hardware Control With Application To Cache Coherence Protocols | Wayne G. Nation, Ken Valk, Irit Shitsevalov, Kyle L. Nelson, Russ Hoover, Cindy Eisner | Design Automation Conference (DAC) | 2000 | Formal |
| Achieving Scalability In Parallel Reachability Analysis Of Very Large Circuits | Tamir Heyman, Danny Geist, Orna Grumberg, Assaf Schuster | Computer Aided Verification (CAV) | 2000 | Formal |
| FoCs - Automatic Generation Of Simulation Checkers From Formal Specifications | Yaron Wolfsthal, Leonid Gluhovsky, Sharon Keidar, Ilan Beer, Yael Abarbanel | Computer Aided Verification (CAV) | 2000 | Formal |
| ""Have I Written Enough Properties?"" - A Method Of Comparison Between Specification And Implementation | Sagi Katz, Orna Grumberg, Danny Geist | Correct Hardware Design and Verification Methods (CHARME) | 1999 | Formal |
| A Methodology For The Verification Of A ``System On Chip'' | Daniel Geist, Giora Biran, Tamarah Arons, Michael Slavkin, Yvgeny Nustov, Monica Farkas, Karen Holtz, Andy Long, Dave King, Steve Barret | Design Automation Conference (DAC) | 1999 | |
| Developing An Architecture Validation Suite Applicaiton To The PowerPC Architecture | Laurent Fournier, Anatoly Koyfman, Moshe Levinger | Design Automation Conference (DAC) | 1999 | |
| Functional Verification Methodology For Microprocessors Using The Genesys Test-Program Generator-Application To The X86 Microprocessors Family | Laurent Fournier, Yaron Arbetman, Moshe Levinger | Design Automation and Test in Europe Conference (DATE) | 1999 | |
| Model Checking The IBM Gigahertz Processor: An Abstraction Algorithm For High-Performance Netlists | Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz | Computer Aided Verification (CAV) | 1999 | Formal |
| Using Symbolic Model Checking To Verify The Railway Stations Of Hoorn-Kersenboogerd And Heerhugowaard | Cindy Eisner | Correct Hardware Design and Verification Methods (CHARME) | 1999 | Formal |
| Design Reliability - Estimation Through Statistical Analysis Of Bug Discovery Data | Yossi Malka, Avi Ziv | Design Automation Conference (DAC) | 1998 | |
| On-The-Fly Model Checking Of RCTL Formulas | Shoham Ben-David, Avner Landver, Ilan Beer | Computer Aided Verification (CAV) | 1998 | Formal |
| User Defined Coverage - A Tool Supported Methodology For Design Verification | Raanan Grinwald, Eran Harel, Michael Orgad, Shmuel Ur, Avi Ziv | Design Automation Conference (DAC) | 1998 | |
| Compacting Regression-Suites On-The-Fly | Erez Buchnik, Shmuel Ur | Asia-Pacific Software Engineering Conference (APSEC) | 1997 | |
| Efficient Detection Of Vacuity In ACTL Formulas | Shoham Ben-David, Cindy Eisner, Ilan Beer, Yoav Rodeh | Computer Aided Verification (CAV) | 1997 | Formal |
| RuleBase - Model Checking At IBM | P. Paanah, G. Ronin, Avner Landver, Yoav Rodeh, Shoham Ben-David, Cindy Eisner, Ilan Beer, Daniel Geist, Yaron Wolfsthal, Leonid Gluhovsky, Tamir Heyman | Computer Aided Verification (CAV) | 1997 | Formal |
| Coverage-Directed Test Generation Using Symbolic Techniques | Yossi Lichtenstein, Avner Landver, Yaron Wolfsthal, Shmuel Ur, Daniel Geist, Monica Farkas | Formal Methods in Computer-Aided Design (FMCAD) | 1996 | Formal |
| RuleBase - An Industry-Oriented Formal Verification Tool | Shoham Ben-David, Cindy Eisner, Avner Landver, Ilan Beer | Design Automation Conference (DAC) | 1996 | Formal |
| AVPGEN-A Test Generator For Architecture Verification | Ashok K. Chandra, Vijay S. Iyengar, D. Jameson, R. V. Jawalekar, Indira Nair, Barry K. Rosen, Michael P. Mullen, J. Yoon, R. Armoni, Daniel Geist, Yaron Wolfsthal | IEEE Trans VLSI Syst 3(2) 188-200 | 1995 | |
| Constraint Satisfaction For Test Program Generation | Daniel Lewin, Laurent Fournier, Moshe Levinger, Evgeny Roytman, Gil Shurek | Phoenix Conference on Computers and Communications (IPCCC) | 1995 | |
| Test Program Generation For Functional Verification Of PowerPC Processors In IBM | Aharon Aharon, Dave Goodman, Moshe Levinger, Yossi Lichtenstein, Yossi Malka, Charlotte Metzger, Moshe Molcho, Gil Shurek | Design Automation Conference (DAC) | 1995 | |
| Efficient Model Checking By Automated Ordering Of Transition Relation Partitions | Daniel Geist, Ilan Beer | Computer Aided Verification (CAV) | 1994 | Formal |
| Methodology And System For Practical Formal Verification Of Reactive Hardware | Shoham Ben-David, Daniel Geist, Ilan Beer, Michael Yoeli, Raanan Gewirtzman | Computer Aided Verification (CAV) | 1994 | Formal |
| Model Based Test Generation For Processor Verification | Yossi Lichtenstein, Yossi Malka, Aharon Aharon | Innovative Applications of Artificial Intelligence (IAAI) | 1994 |