Registration is now open.

The Haifa Verification Seminar (HVS) is a leading seminar dedicated to advancing the state-of-the-art and state-of-the-practice in verification and testing.

The seminar provides a forum for researchers and practitioners from academia and industry to share their work, exchange ideas, and discuss the future directions of quality, testing, and verification for hardware, software, cloud, quantum, automotive, and complex hybrid systems. The common underlying goal of these techniques is to ensure the correct functionality and performance of complex systems. The new face of these domains spans exciting technologies, including AI and analytics, encouraging the migration of methods and ideas among domains.

HVS, following the 13 years of the Haifa Verification Conferences, offers a full day of talks and discussions about the newest breakthroughs in industry and academia. Topics will include areas such as edge computing, cloud, analytics, automotive, verification in the quantum era, and AI usage in theses fields.

The seminar will take place in the auditorium of IBM Research – Haifa on the University of Haifa campus. Lunch and light refreshments will be served. Participation is free but registration is required.

Parking is available in the IBM Research - Haifa lot.

We look forward to seeing you at the seminar!

Organization Committee

  • Raviv Gal, IBM Research - Haifa
  • Sharon Keidar Barner, IBM Research - Haifa
  • Rachel Tzoref-Brill, IBM Research - Haifa
  • Avi Ziv, IBM Research - Haifa
  • Revivit Yankovich, IBM Research - Haifa

Program

The Haifa Verification Seminar (HVS) is a leading seminar dedicated to advancing the state-of-the-art and state-of-the-practice in verification and testing. Following 13 years of Haifa Verification Conferences, HVS offers a full day of talks and discussions about the newest breakthroughs in industry and academia. Topics will include areas such as edge computing, cloud, analytics, automotive, verification in the quantum era, and AI usage in these fields.

08:30    Registration
09:00 Opening Remarks
Moshe Levinger, IBM Research - Haifa
09:15Keynote: Design Automation for Quantum Computing
Robert Wille, Johannes Kepler University (JKU) Linz
10:15 Testing in the Open Source World
Shai Revivo, Red Hat
Abstract:
Open unlocks world potential! We are often harnessing the power of open source in finding new solutions and solving joint problems. But, what about quality? Since contribution is not limited to a certain people, company, organization or country how do we bring it all together to form a high quality enterprise software? In this talk you will get a high level overview on how we do it in Red Hat.
10:45Break

11:15 Protecting against HW-level Malicious Partner Remote Attacks on Data Centers
Sergio Carpovich, Intel
Abstract:
In the past few years, the number, ingenuity and sources of “malicious partner” remote attacks on Data Centers has increased dramatically. Such attack held by a country, a company or even a single hacker can heavily damage the functionality of a data center. These attacks try to “remotely” (i.e. without physically accessing the silicon, by just sending an Ethernet packet from a link partner to the NIC or a local guest OS) exploit potential HW vulnerabilities in Ethernet controllers. These, if not detected in time before mass production, expose Intel as the supplier of the silicon and the customer as the data center owner to great risks. In some cases, even a guest OS utilizing the NIC might be “malicious” (i.e. trying to harm the NIC), so such packets can be seen not just in the NIC’s RX path, but also in its TX path. Therefore, in this talk we will explain the nature of these HW vulnerabilities, including unfortunately real ‘escapes’ from past products, and the way they are tackled in pre-silicon verification simulations as to detect them before shipping the product.
11:45 PSS? What’s in It for Me?
Sharon Rozenberg, Cadence
12:15 Lamplighter: Using Unsupervised Learning and Markov Chains to Generate Client-based Tests
Guy Barash, Western Digital
Eyal Gomel, Western Digital
Abstract:
Designing a great test is hard, a team of skilled testers can design countless tests that will check everything imaginable by them, but the client might do something else and find a bug. Lamplighter is an attempt to solve the issue top down and not bottom up – it uses advances in the field of machine learning to attempt to observe the client behavior, model it, and generate tests based on observed client behavior.
12:45 Frea-AI: Bridging the Gap between ML Solutions and Their Business Requirements
Orna Raz, IBM Research - Haifa
Abstract:
Machine learning (ML) solutions are prevalent. However, many challenges exist in making these solutions business-grade. One major challenge is to ensure that the ML solution provides its expected business value. In order to do that, one has to bridge the gap between the way ML model performance is measured and the solution requirements. We demonstrate the effectiveness of utilizing feature models, either maunally defined or automatically suggested via FreaAI, in bridging this gap. Whereas ML performance metrics, such as the accuracy or F1-score of a classifier, typically measure the average ML performance, feature models shed light on explainable data slices that are too far from that average, and therefore might indicate unsatisfied requirements. For example, the overall accuracy of a bank text terms classifier may be very high, say 98% +- 2%, yet it might perform poorly for terms that include short descriptions and originate from commercial accounts. A business requirement, which may be implicit in the training data, may be to perform well regardless of the type of account and length of the description. Therefore, the under-performing data slice that includes short descriptions and commercial accounts suggests poorly-met requirements. FreaAI implements heuristics for automatically extracting feature models that result in explainable and statistically significant data slices over which the ML solution under-performs.
13:15Lunch

14:15 Keynote: How to Catch a Lion in the Desert - On the Solution of the Coverage-Directed Generation (CDG) Problem
Eldad Haber, University of British Colombia (UBC), Vancouver
Abstract:
The testing and verification of a complex hardware or software system can be a difficult process. One of the most difficult and time-consuming tasks a verification team faces is reaching coverage closure, or hitting coverage events that have not been hit before. Coverage-directed-generation (CDG), or the automatic generation of tests that can hit previously unhit coverage events, holds the potential to save verification teams significant simulation resources and time. In this talk, we propose a new approach to the CDG problem that utilizes techniques from derivative free optimization coupled with a robust noise estimator, and demonstrate the effectiveness of this new approach through numerical experiments with IBM’s NorthStar processor.
15:15 SYNTECH: Synthesis Technologies for Reactive Systems Software Engineers
Shahar Maoz, Tel Aviv University
Abstract:
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given declarative, temporal specification. Examples of these systems include the software controllers of robotic systems. Despite recent advancements on the theory and algorithms of reactive synthesis, e.g., efficient synthesis for the GR(1) fragment of linear temporal logic, many challenges remain in bringing reactive synthesis technologies to the hands of software engineers. The SYNTECH project is about bridging this gap. It addresses challenges that relate to the change from writing code to writing specifications, and the development of tools to support a specification-centric rather than a code-centric software development process. In this talk I will give an overview of the SYNTECH project’s results from the last four years. These include the Spectra specification language and Spectra Tools, a synthesizer and related analyses aiming at helping engineers write better specifications for synthesis. I will also present the application of Spectra to autonomous Lego robots and some example simulated systems, as developed by undergraduate computer science students in project classes we have taught. The talk will cover results from papers in ESEC/FSE’15, SYNT’15, ESEC/FSE’16, SYNT’16, ESEC/FSE’17, SYNT’17, ICSE’19, and FM'19. Joint work with Gal Amram, Elizabeth Firman, Aviv Kuvent, Or Pistiner, Jan O. Ringert, and Rafi Shalom. The project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 638049, SYNTECH).
16:00Break

16:30 M-SDL - A Language (and Philosophy) for Verifying Autonomous Vehicles
Yoav Hollander, Foretellix
Abstract:
Currently, the main obstacle to deploying autonomous vehicles seems to be verification (and related topics like regulation). Coverage-driven verification, using a common scenario description language, could be a central part of the solution. This talk will present M-SDL (the Measurable Scenario Description Language), and the philosophy behind it, and why a new verification language is even needed.
17:15 Quality and Trust for Autonomous Systems
Maayan Goldstein, Nokia Bell Labs
Abstract:
Autonomous systems are becoming pervasive in our daily life, also in domains that can be considered safety-critical, like healthcare, automotive, etc. Many of those systems use machine learning models to make decisions that could have very negative consequences, even catastrophic, if wrong. Our objective is to understand how much, and in which conditions, an autonomous system can rely on machine learning models. At present, we work on developing safety shells that ensure that whenever a machine learning component makes a decision that might have adverse effects, nothing “bad” propagates to the system level. These shells can improve the overall quality of the autonomous systems and increase the trust users have in them. In this talk I will present our first step towards this ambitious goal - a tool for quantifying the robustness of tree ensemble-based models
17:45 Concluding Remarks
Raviv Gal, IBM Research – Haifa

Registration

Registration is now open.

Registration Link

Click here

Time and Location

Tuesday November 19, 2019
8:30 to 18:00
At IBM Research in Haifa, auditorium
Haifa University Campus,
Mount Carmel Haifa, Israel
View Map

Keynotes Speakers

  • Prof. Robert Wille, Institute for Integrated Circuits, Johannes Kepler University (JKU) Linz.
  • Prof. Eldad Haber, Department of Earth, Ocean and Atmospheric Sciences, the University of British Colombia (UBC), Vancouver

Previous Conferences