Mission

The long-term mission of the center is to advance and promote the state of the art of formal verification of reactive systems until it can be transformed from an academic disciplines with a few success stories into a working practice that will gradually take its right place within industrial practice as an established recognized stage in the development life-cycle of reactive systems.

To promote this dramatic progress and eventual transformation, we intend to take a central place in the development of the new discipline of verification engineering. The plan for bringing about this development includes:

• Conducting basic and applied research for the development of new specification languages, new paradigms for formal verification, emphasizing compositionality, abstraction, and other techniques for reducing intractably large designs into manageable units.

  Our main research thrust in the formal verification direction will be centered around deductive verification techniques combined with conscientious efforts of merging this family of techniques with enumerative approaches such as model checking (explicit state as well as symbolic), symbolic execution, and other similar approaches.

  On the modeling side, we will continue in the development of formal models for reactive systems, extending and enhancing the hierarchy consisting of discrete events, real-time, and hybrid systems.

  On the subject of methodologies, we will study and explore the uses of formal methods for property verification, verification of equivalence refinement and abstraction between systems, user guided approaches to rigorous system development, and automatic synthesis of small systems from their specifications.

• The gathering together of the existing tools and methods for formal verification, conducting a thorough and comparative analysis and assessment for identifying their strengths and weaknesses, and forming stable recommendations and guidelines for the ranges of their applicability.

• The development of new tools and methods that will complement the existing technologies, typically combining together differing approaches, such as the deductive and explorative approaches, or focusing on particular application domains where a specialized approach may prove beneficial.

• The development of a verification engineering methodology and curriculum, which will identify the fields of knowledge a practicing verification engineer needs as a background, and include a carefully planned set of courses of action one would systematically pursue in verifying a system of given characteristics.

• In its capacity as a consulting foundation, the center will advise interested industries (Israeli and German) in the selection of the formal approach that best fits their type of systems, in setting up a formal activity within their companies, and accompanying them in initiating some pilot projects for the use of formal verification in system development.

• Dissemination and education of the technical industrial public in the ways of formal verification by a series of workshops and concentrated short in-depth courses which will introduce selected methods and tools.

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