Program Day 3 - Thursday 17/11/2016

09:00 - 10:00 Keynote: miTLS: Can cryptography, formal methods, and applied security be friends?
Dr. Markulf Kohlweiss, Researcher, Microsoft Research
Session Chair: Sharon Keidar-Barner

10:00-11:15 Technical session: Software Verification
Session chair: Nikolaj Bjorner

Formula Slicing: Inductive Invariants from Preconditions,
Egor George Karpenkov and David Monniaux

Advancing software model checking beyond linear arithmetic theories,
Ahmed Mahdi, Karsten Scheibler, Felix Neubauer, Martin Fränzle and Bernd Becker

Predator Shape Analysis Tool Suite,
Lukas Holik, Michal Kotoun, Petr Peringer, Veronika Šoková, Marek Trtík and Tomas Vojnar

11:15 - 12:00 Coffee Break

12:00 - 13:30 Special Industry Session
Session chair: Merav Aharoni

Challenges and Opportunities in System Validation and Debug: a Collaborative Approach,
Aviv Barkai, Intel

Abstract: Semiconductor companies invest increasingly more and more into post-silicon validation, coverage and debug. Each company develops its own methodologies and tools, while electronic design automation (EDA) vendors have very few offerings for these areas. Academic research is also relatively weak in these domains.

Over the last year, there has been renewed interest in creating a collaborative effort, including several companies as well as academia, specifically on topics such as:
1) Using design for test (DFT) for system debug
2) Defining standard test suites
3) Defining validation data analytics
4) Coverage definition, measurement and interpretation

The System Validation and Debug Technology Committee (SVDTC) is an IEEE-CEDA committee that brings together experts from industry and academia to address these issues, specifically for on-silicon platforms. In my talk, I will describe the challenges and work done within this organization.

SVA for FV: Beyond Assertions,
Max Chvalevsky, Marvell

Abstract: Any formal verification tool must support several features in order to be effective for various designs. The most basic among them are capabilities to define assertions and environment; ability to override design signals; and support for associating every assertion with the environment appropriate to it. Today, most industry FV tools use System Verilog Assertions (SVA) as the description language. While this language is very rich, it was not designed with FV in mind. Instead, it was aimed mainly at simulation. As a result, most vendors use Tcl scripting in order to complement SVA and support all the required FV features. This solution, despite some advantages, requires combining two intertwined source codes in order to define any non-trivial FV task. An alternative new approach is to use System Verilog Checkers, with some additions beyond the standard, in order to provide a single-code SVA solution for formal verification. This solution, being based on System Verilog, exploits the power and expressiveness of the language while meeting all the FV requirements.

Testing Big Data Systems,
Akram Bitar, IBM Research - Haifa

Abstract: Acquiring and managing test data has become a major challenge for organizations. Embracing agile development methodologies and continuous delivery introduce new difficulties in availability, quality, and volume of test data. These difficulties impose stringent performance and scalability requirements on data acquisition solutions. Furthermore, new data protection regulations render most state-of-the-art solutions inadequate. We survey the state-of-the-art test data management technologies, including their strengths and their weaknesses. We present a new approach for fabrication of high-quality test data that enables generating high-quality data from scratch, as well as utilizing existing data. This approach uses a constraint satisfaction problem solver as its core data generator.

13:30 - 15:00 Lunch

15:00 - 16:00 HVC Award Ceremony & presentation
Session chair: Roderick Bloem

16:00 Closing remarks

Keynote Speakers


See us on Linked In See us on Facebook IBM Research Cadence Mellanox Mentor Graphics Qualcomm SunDisk