Interaction with Industry

The contacts maintained throughout 1999-2000 include the following:

C1.

Intel - the Haifa advanced technology center. The contact person there is Dr. Limor Fix. Our research projects that are of interest to (and partially supported by) them are our work on deductive and algorithmic verification of out-of-order designs, and the work on verification of parameterized systems. Our contact persons are A. Pnueli, T. Arons, and N. Piterman.

C2.

IBM Research Center in Haifa. The contact person there is Y. Wolfsthal. Their main interest is our work on deductive verification of hardware designs. Our contact persons are A. Pnueli, Y. Rodeh, D. Fisman, and O. Shtrichman who cooperates with the IBM group on the topic of Bounded Model Checking [Sht00].

C3.

Verisity. This company produces tools for testing hardware designs. Our cooperation with them involved the design of a new language for the specification of tests. Our contact person is Y. Kesten.

C4.

Perfecto. This is a start-up company that plans to market tools for ensuring security and immunity from interference on the net. Their plan was to have their complete software system formally verified. Our contact persons are A. Pnueli and Y. Kesten. The interaction was very successful and resulted in verification of some of their subsystems, as reported in [KKPR99b] and [KKPR99a].

C5.

I-Logix. Both D. Harel and A. Pnueli are on the scientific board of this company, whose development division is located in Rehovot. Through the participation of I-Logix in the European project Sacres and intense argumentation of A. Pnueli and W. Damm, the company is about to add a model checking component to their product (Statemate). Examples of research which is of value and extensive interest to I-Logix are [DH98], [DJHP98], and [Har01].

C6.

Israeli Aircraft Industries (IAI). There is a long tradition of cooperation between IAI and the CS group at Weizmann. The whole concept of Statecharts was developed as part of a consultation by D. Harel to IAI in 1983 which continued by IAI sponsoring the commercial development of the Statecharts specification tool Statemate, in an effort that eventually led to the setting up of the I-Logix company.

This cooperation renewed with IAI and Weizmann being both partners in the current EC (European Community) project Safeair, where Weizmann contributes the translation validation technology. This cooperation will tighten through the recently approved EC project Omega focusing on the development of a real-time UML-oriented system development methodology, where the Weizmann group will contribute verification, synthesis, and language definition technologies and IAI will identify user needs and experience in training practitioners to use rigorous system development methods.

So far, our contacts have been mainly with Israeli industries (or Israeli branches of international companies). We have had some contacts with Siemens through the joint European projects Sacres and Safeair.

The nature of the cooperation with these companies varies according to conditions and expectations. With both Intel and IBM we have a research agreement, according to which we conduct at our site a research which is of interest to them. At regularly spaced meetings we inform them of our results and obtain feedback. In 1999, we sent T. Arons to spend some time at the Intel center, where she interacted with some of their designers and obtained betters insights about the appropriateness of the methodologies she developed to their typical problems.

In the case of Verisity, we used to have regular working sessions in which we worked together some of the ideas which they proceeded to implement and study.

For the ambitious verification project of Perfecto, we served as consultants but the main verification work is done by them at their plant.

Dept. of Computer Science and Applied Math The Weizmann Institute of Science Rehovot 76100, Israel TelePhone: +972-8-934-3434 Telefax: +972-8-934-4122 To comment on this service, send feedback to the Nir Piterman