Verification Technology (Computer Systems Design sub-discipline) Publications



2016

Control flow error localization
Friedler, Ophir and Kadry, Wisam and Nahir, Amir and Sokhin, Vitali
US Patent 9,251,045

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


2015

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
2015 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 321--324


2014

Verification of transactional memory in power8
Adir, Allon and Goodman, Dave and Hershcovich, Daniel and Hershkovitz, Oz and Hickerson, Bryan and Holtz, Karen and Kadry, Wisam and Koyfman, Anatoly and Ludden, John and Meissner, Charles and others
2014 51st ACM/EDAC/IEEE Design Automation Conference (DAC), pp. 1--6

Method and apparatus for post-silicon testing
Adir, Allon and Bin, Eyal and Copty, Shady and Koyfman, Anatoly and Landa, Shimon and Nahir, Amir and Sokhin, Vitali and Tsanko, Elena
US Patent 8,892,386

Using a high-level test generation expert system for testing in-car networks
Adir, Allon and Goryachev, Alex and Greenberg, Lev and Salman, Tamer
Proceedings of the 51st Annual Design Automation Conference, pp. 1--6, 2014

Effective post-silicon failure localization using dynamic program slicing
Ophir Friedler and Wisam Kadry and Arkadiy Morgenshtein and Amir Nahir and Vitali Sokhin
Proceedings of the conference on Design, Automation & Test in Europe, pp. 319, 2014


2013

Verifying correctness of processor transactions
Adir, Allon and Ludden, John Martin and Ziv, Avi
US Patent 8,589,734

Architectural failure analysis
Friedler, Ophir and Kadry, Wisam and Nahir, Amir and Sokhin, Vitali
US Patent App. 14/141,981


2012

Generating a combination exerciser for executing tests on a circuit
Adir, Allon and Golubev, Maxim and Klinger, Andrey and Nahir, Amir
US Patent 8,224,614

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, pp. 178--192, 2012

Mage-the CDCL SAT solver developed and used by IBM for formal verification http://ibm. co
Margalit, Oded and Matsliah, Ari{"e}
P7qNpC. personal communication, 2012

nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces
F. De Paula, A. Hu, A. Nahir
Computer Aided Verification, pp. 513--531, 2012

Approximating Checkers for Simulation Acceleration
B. Mammo, D. Chatterjee, D. Pidan, A. Nahir, A. Ziv, R. Morad, V. Bertacco
DATE, pp. 153-158, 2012


2011

Threadmill: a post-silicon exerciser for multi-threaded processors
Adir, Allon and Golubev, Maxim and Landa, Shimon and Nahir, Amir and Shurek, Gil and Sokhin, Vitali and Ziv, Avi
Proceedings of the 48th Design Automation Conference, pp. 860--865, 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 48th ACM/EDAC/IEEE, pp. 569--574

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 48th ACM/EDAC/IEEE, pp. 569--574

Stimuli generation for functional hardware verification with constraint programming
Adir, Allon and Naveh, Yehuda
Hybrid Optimization, pp. 509--558, Springer, 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 \& Test in Europe Conference \& Exhibition (DATE), 2011, pp. 1--6

Threadmill: A post-silicon exerciser for multi-threaded processors
A. Adir, M. Golubev, S. Landa, A. Nahir, G. Shurek, V. Sokhin, A. Ziv
Design Automation Conference (DAC), 2011 48th ACM/EDAC/IEEE, pp. 860--865


2010

Reaching coverage closure in post-silicon validation
A Adir, A Nahir, A Ziv, C Meissner, J Schumann
Hardware and Software: Verification and Testing, 60--75, Springer, 2010


2009

Model-Based Hardware Exerciser, Device, System and Method Thereof
A Adir, G E Shurek
2009 - freepatentsonline.com

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, 2009. MEMOCODE'09. 7th IEEE/ACM International Conference on, pp. 78--87

User-friendly model checking: Automatically configuring algorithms with RuleBase/PE
Z Nevo
Hardware and Software: Verification and Testing, 210--214, Springer, 2009

Using Bayesian networks and virtual coverage to hit hard-to-reach events
S Fine, L Fournier, A Ziv
International Journal on Software Tools for Technology Transfer (STTT) 11(4), 1--15, Springer, 2009

Explaining counterexamples using causality
I Beer, S Ben-David, H Chockler, A Orni, R Trefler
Computer Aided Verification, pp. 94--108, 2009

Cross-Entropy-Based Replay of Concurrent Programs
H Chockler, E Farchi, B Godlin, S Novikov
Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, pp. 201--215

Before and after vacuity
H Chockler, O Strichman
Formal Methods in System Design 34(1), 37--58, Springer, 2009

Source Springer-Verlag Berlin, Heidelberg
H Chockler, A J Hu
Proceedings of the 4th International Haifa Verification Conference on Hardware and Software: Verification and Testing, 2009

Formal verification of correctness and performance of random priority-based arbiters
Krishnan Kailas, Viresh Paruthi, Brian Monwai
Proc. of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), pp. 101-107, IEEE

Functional verification of power gated designs by compositional reasoning
Cindy Eisner, Amir Nahir, Karen Yorav
Computer Aided Verification: 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings, pp. 40-55, Springer, 2009


2008

Policy Validation for System Automation: A Case Study
E Zarpas, C Eisner, S Tal
Policies for Distributed Systems and Networks, 2008, pp. 46--53

Efficient Automatic STE Refinement Using Responsibility
H Chockler, O Grumberg, A Yadgar
Tools and algorithms for the construction and analysis of systems: 14th international conference, TACAS 2008, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008: proceed, pp. 233

Beyond vacuity: Towards the strongest passing formula
H Chockler, A Gurfinkel, O Strichman
Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, pp. 1--8

What causes a system to satisfy a specification?
H Chockler, JY Halpern, O Kupferman
ACM TOCL, 2008

A probabilistic alternative to regression suites
S. Copty, S. Fine, S. Ur, E. Yom-Tov, A. Ziv
Theoretical Computer Science 404(3), 219--234, Elsevier, 2008


2007

A framework for the validation of processor architecture compliance
Allon Adir, Sigal Asaf, Laurent Fournier, Itai Jaeger, Ofer Peled
Design Automation Conference, pp. 902--905, 2007

Automatic Generation of Test Suite for Processor Architecture Compliance
A Adir, S Asaf, L Fournier, I Jaeger
US Patent App. 11/735,510

Easier and More Informative Vacuity Checks
H Chockler, O Strichman
Proceedings of MEMOCODE, 2007

ExpliSat: Guiding SAT-based software verification with explicit states
S Barner, C Eisner, Z Glazberg, D Kroening, I Rabinovitz
Hardware and Software, Verification and Testing4383, 138--154, Springer, 2007


2006

Addressing Test Generation Challenges for Configurable Processor Verification
M Rimon, Y Lichtenstein, A Adir, I Jaeger, M Vinov, S Johnson, D Jani
IEEE International High-Level Design Validation and Test Workshop, pp. 95--101, 2006

A practical introduction to PSL
C Eisner, D Fisman
2006 - books.google.com, Springer-Verlag New York Inc

Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based &
PC Attie, DH Lorenz, A Portnova, H Chockler
Proceedings of CBSE, 2006

Coverage metrics for temporal logic model checking*
H Chockler, O Kupferman, MY Vardi
Formal Methods in System Design, 2006 - Springer

Automatic Verification of Fault-Tolerant Register Emulations
PC Attie, H Chockler
Electronic Notes in Theoretical Computer Science, 2006 - Elsevier

Formal verification of concurrent software: two case studies
H Chockler, E Farchi, Z Glazberg, B Godlin, Y Nir
Proceedings of PADTAD, 2006

Coverage metrics for formal verification
H Chockler, O Kupferman, M Vardi
International Journal on Software Tools for Technology …, 2006 - Springer

Distributed dynamic BDD reordering
Z Nevo, M Farkash
Design Automation Conference, 2006 43rd, pp. 223--228, ACM/IEEE

Advanced analysis techniques for cross-product coverage
H Azatchi, L Fournier, E Marcus, S Ur, A Ziv, K Zohar
IEEE Transactions on Computers 55(11), 1367--1379, IEEE INSTITUTE OF ELECTRICAL AND ELECTRONICS, 2006


2005

A generic micro-architectural test plan approach for microprocessor verification
A Adir, H Azatchi, E Bin, O Peled, K Shoikhet
Proceedings of the 42nd annual Design Automation Conference, pp. 774, 2005

VLIW: a case study of parallelism verification
A Adir, Y Arbetman, B Dubrov, Y Lichtenstein, M Rimon, M Vinov, M A Calligaro, A Cofler, G Duffy
Proceedings of the 42nd annual Design Automation Conference, pp. 782, 2005

SATABS: SAT-based predicate abstraction for ANSI-C
E Clarke, D Kroening, N Sharygina, K Yorav
TACAS, 2005 - Springer

Assumption-based distribution of CTL model checking
L Brim, K Yorav, J dkov
International Journal on Software Tools for Technology …, 2005 - Springer


Automatic test program generation using extended conditional constraint satisfaction
A Adir, E Bin, R Emek, K Shoikhet
US Patent App. 11/040,241, 2005 - Google Patents, Google Patents
US Patent App. 11/040,241

A topological characterization of weakness
Cindy Eisner, Dana Fisman, John Havlicek
Proceedings of the twenty-fourth annual ACM symposium on Principles of distributed computing, pp. 1--8, ACM, 2005
Abstract

Temporal Modalities for Concisely Capturing Timing Diagrams
H Chockler, K Fisler
LECTURE NOTES IN COMPUTER SCIENCE, 2005 - Springer


2004

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
Design \& Test of Computers, IEEE 21(2), 84--93, IEEE, 2004

Efficient Verification of Sequential and Concurrent C Programs
Clarke, A Groce, J Ouaknine, O Strichman, K Yorav
Formal Methods in System Design, 2004 - Springer

Static Analysis for State-Space Reductions Preserving Temporal Logics
K Yorav, O Grumberg
Formal Methods in System Design, 2004 - Springer

Efficiently verifiable suficient conditions for deadlockfreedom of large concurrent programs
PC Attie, H Chockler
Technical report, Northeastern University, Boston, MA, 2004. …

A lower bound for testing juntas
Hana Chockler, Dan Gutfreund
Inf. Process. Lett. 90(6), 301--305, 2004

\omega-Regular languages are testable with a constant number of queries
H Chockler, O Kupferman
Theoretical Computer Science, 2004 - Springer

Probabilistic regression suites for functional verification
Shai Fine, Shmuel Ur, Avi Ziv
Proceedings of the 41st annual Design Automation Conference, pp. 49-54, Google Patents, 2004
US Patent App. 11/145,866


2003

Automated compositional abstraction refinement for concurrent C programs: A two-level approach
S Chaki, J Ouaknine, K Yorav, E Clarke
Electronic Notes in Theoretical Computer Science 89(3), 417--432, Elsevier, 2003

The definition of a temporal clock operator
C Eisner, D Fisman, J Havlicek, A McIsaac, D Van Campenhout
Automata, Languages and Programming, 193--193, Springer, 2003

Reasoning with temporal logic on truncated paths
C Eisner, D Fisman, J Havlicek, Y Lustig, A McIsaac, D Van Campenhout
Computer Aided Verification, pp. 27--39, Springer, 2003

Model Checking at IBM
S Ben-David, C Eisner, D Geist and Y Wolfsthal
Formal Methods in System Design 22(2), 101--108, Springer, 2003

Coverage metrics for formal verification
H Chockler, O Kupferman, MY Vardi
Proceedings of CHARME, 2003

Responsibility and blame: a structural-model approach
H Chockler, JY Halpern
Arxiv preprint cs/0312038, 2003 - arxiv.org


2002

Adaptive test program generation
A Adir, R Emek, E Marcus
US Patent App. 10/040,940, 2002 - Google Patents, Google Patents
US Patent App. 10/040,940

Using Assumptions to Distribute CTL Model Checking
L Brim, J Crhov, K Yorav
Electronic Notes in Theoretical Computer Science, 2002 - fi.muni.cz

Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard
C Eisner
International Journal on Software Tools for Technology Transfer (STTT) 4(1), 107--124, Springer, 2002

Comparing symbolic and explicit model checking of a software system
C Eisner, D Peled
Model Checking Software, 79--82, Springer, 2002

Establishing PCI compliance using formal verification: a case study
I Beer, S Ben-David, C Eisner, Y Engel, R Gewirtzman, A Landver
Computers and Communications, 1995, pp. 373--377, 2002

\omega- Regular Languages Are Testable with a Constant Number of Queries
H Chockler, O Kupferman
Randomization and Approximation Techniques in Computer …, 2002 - books.google.com

Which bases admit non-trivial shrinkage of formulae?
H Chockler, U Zwick
Computational Complexity, 2002 - portal.acm.org

Coverage of Implementations by Simulating Specifications
H Chockler, O Kupferman
Proceedings of the IFIP 17th World Computer Congress-TC1 …, 2002 - portal.acm.org

Coverage measurement tool for user defined coverage models
Y. Malka, A. Gluska, S. Ur, A. Ziv, others
US Patent 6,356,858

Cross-Fertilization between Hardware Verification and Software Testing
S Ur, A Ziv
6th IASTED International Conference on Software Engineering and Applications (SEA2002)

Hole analysis for functional coverage data
O. Lachish, E. Marcus, S. Ur, A. Ziv
Design Automation Conference, 2002. Proceedings. 39th, pp. 807--812


2001

Model checking the garbage collection mechanism of SMV
C Eisner
Electronic Notes in Theoretical Computer Science 55(3), 289--303, Elsevier, 2001

Reproducing Synchronization Bugs with Model Checking
K Yorav, S Katz, R Kiper
LECTURE NOTES IN COMPUTER SCIENCE, 2001 - Springer

On the Effective Deployment of Functional Formal Verification
Y Abarbanel-Vinov, N Aizenbud-Reshef, I Beer, C Eisner, D Geist, T Heyman, I Reuveni, E Rippel, I Shitsevalov and Y Wolfsthal
Formal Methods in System Design 19(1), 35--44, Springer, 2001

Efficient detection of vacuity in temporal model checking
I Beer, S Ben-David, C Eisner, Y Rodeh
Formal Methods in System Design 18(2), 141--163, Springer, 2001

The temporal logic Sugar
I Beer, S Ben-David, C Eisner, D Fisman, A Gringauze, Y Rodeh
Computer Aided Verification, pp. 363--367, Springer, 2001

Which formulae shrink under random restrictions?
H Chockler, U Zwick
Proceedings of the twelfth annual ACM-SIAM symposium on …, 2001 - portal.acm.org

Coverage metrics for temporal logic model checking
MY Vardi, H Chockler, O Kupferman
Proc. of TACAS01, 2001

A Practical Approach to Coverage in Model Checking
H Chockler, O Kupferman, RP Kurshan, MY Vardi
Proceedings of CAV, 2001

Cost Evaluation of Coverage-Directed Test Generation for the IBM Mainframe
G Nativ, S Mittermaier, S Ur, A Ziv
International Test Conference, pp. 793--802, 2001


2000


A methodology for formal design of hardware control with application to cache coherence protocols
Cindy Eisner, Irit Shitsevalov, Russ Hoover, Wayne Nation, Kyle Nelson, Ken Valk
Proceedings of the 37th Annual Design Automation Conference, pp. 724--729, ACM, 2000
Abstract


1998

User defined coverage-a tool supported methodology for design verification
M Orgad, A Ziv, S Ur, E Harel, R Grinwald
dac, pp. 158--163, 1998

Off-the-shelf vs. custom made coverage models, which is the one for you
S Ur, A Ziv
proceedings of STAR98: the 7th international conference on software testing analysis and review, 1998


1997

RuleBase: Model Checking at IBM
I Beer, S Ben-David, C Eisner, D Geist, L Gluhovsky, T Heyman, A Landver, P Paanah, Y Rodeh, G Ronin and Y Wolfsthal
Computer Aided Verification (CAV '97), pp. 480--483, Springer, 1997


1996

RuleBase: an industry-oriented formal verification tool
Ilan Beer, Shoham Ben-David, Cindy Eisner, Avner Landver
Proceedings of the 33rd annual Design Automation Conference, pp. 655--660, ACM, 1996