Over the recent decade, Model Checking has established itself as the industry's solution of choice for functional formal verification. Indeed, computer companies such as IBM, Intel, and Motorola, as well as a good number of fabless design companies such as Galileo Technology and Zoran microelectronics, are actively deploying Model Checking. Overall, the usefulness and practicality of Model Checking are already proven, and the literature features a good number of case studies to that effect.

As a relatively young discipline, the science of Model Checking is also evolving rapidly, and new research trends bring new challenges into focus, such as satisfiability-based model checking, parallel verification algorithms and others. These problems require new approaches, amongst them perhaps the most challenging ones being how to deal with really-large state spaces; and how to make the technology viable to users at large.

Accordingly, the goal of this Summer Seminar is to foster collaboration between industry and academia in what the industry now perceives to be a critical technology for verification. We plan to have industry sessions, reports on recent research, encouraging recent and informal results. In the relaxed setting of Haifa—on the Mediterranean by the Carmel Mountains—we are hoping to elicit a fruitful exchange of information beneficial to all involved.

Seminar Organizing Committee:
      Yaron Wolfsthal
      Yael Vinov-Abarbanel

Local Arrangements:
      Ettie Gilead

Logistics Administrator:
      Liat Grosso

WebMaster:
      Roy Cagan