|
News |
IBM Haifa Research Laboratory
The IBM Haifa Research Laboratory (HRL) is a subsidiary of IBM Israel. The main mission of HRL is to perform research that advances IBM's products and product development capabilities. HRL reports into the IBM Corporation's Research Division and has close working relationships with IBM Israel and its twin research laboratory in Zurich. HRL's Formal Methods Group has experience in model-checking; this group is a part of the Verification Technologies Department headed by Yossi Malka.
The Verification Technologies department is a key participant, a leader, and a recognized centre of competence in all verification activities of the IBM corporation worldwide. Over the past 17 years, there has been a steady dissemination of information, tools, and methodologies from HRL (formerly IBM Science and Technology) to the corporation's European centres, including Essones France and the large design centre in Boeblingen, Germany. The department has marketed its tools to external customers, including a number of design companies in Israel and ST Microelectronics in France, the UK, and Italy.
The department is currently engaged in two framework projects, Genevieve (design verification) under the 4th Framework and Odette (high level modelling) under the 5th Framework.
The Formal Methods Group is well known both inside and outside IBM as the developer of RuleBase, the IBM proprietary world-class model checker. RuleBase is used in virtually all IBM processor projects as well as in ASIC groups inside and outside IBM, and has been licensed to other companies (e.g., ST Microelectronics and Zoran Microelectronics). RuleBase was recently mentioned in the announcement of the ACM Kannelakis Award given to prominent computer scientists E. Clarke, K. McMillan, R. Bryant, and A. Emerson. RuleBase was mentioned as a tool where advanced testing technologies have been implemented and successfully put to practical use.
HRL's Systems Applications Group is engaged in developing software systems with a high technological content including call centre control systems, customer access applications, and mathematical optimisation of scheduling systems. In developing these systems, the group has been extensively involved in testing a wide range of products and in supplying IBM internal tools for software testing. The Formal Methods Group and the Systems Applications Group jointly developed an automated software testing system known as GOTCHA-TCBeans.