VERIMAG is a large academic research laboratory having the status of a joint research unit (JRU) affiliated with the university of Grenoble (UJF), the national center for scientific research (CNRS) and the engineering school of Grenoble (INPG). The INPG will have the administrative responsibility for the activities of VERIMAG in the project.

The research at VERIMAG, conducted by more than 40 researchers and graduate students, addresses all theoretical and practical aspects of formal methods for system development. VERIMAG has a proven record in both fundamental results and in development of tools such as the verification package CADP, the data-flow synchronous language LUSTRE (used for programming embedded control systems), the KRONOS tool for verification of timed automata and the recently-developed d/dt prototype tool for analysis of continuous and hybrid systems. VERIMAG is composed of three groups with strong mutual interaction: 1) The synchronous programming group concentrating on the Lustre/Scade programming environment for writing safety-critical embedded applications. The main feature of Lustre is the combination of a control-oriented date-flow language based on block diagrams, rigorous semantics and efficient compilation; 2) The distributed systems group focusing on verification of asynchronous communication protocols (such as those written in SDL) and of smart card applications; 3) The timed and hybrid systems group whose research agenda includes the exportation of verification methodology toward new application domains, including timing analysis, optimization and control system design.

VERIMAG has a long history of successful participation and coordination of European projects, and among the recent European project in which it participated one can find the projects SYRF, VIRES, CRISYS and VHS (verification of hybrid systems), for which it was a coordinator. VERIMAG has strong working relations with leading centers in hybrid systems research in the US such as Berkeley, Stanford, CMU and Penn, as well as ongoing interaction with industry including Telelogic, France Telecom, Schneider, Aerospatiale, Gemplus, EDF and others.

The hybrid systems group of VERIMAG has been the principal promoter of hybrid systems research in Europe and has organized or participated in the organization of most hybrid system workshops in Europe and the US. In particular it coordinated the first Esprit-NSF network on the topic (1992) as well as the recent VHS project, for which the proposed project can be viewed as a successor. Members of the group edited two special issues on hybrid systems in the journals Theoretical Computer Science (1995) and the European Journal of Control (2001). The timed automata verification tool Kronos developed by the group was among the first hybrid verification tools and a source of inspiration for many other tools. Current research effort in the hybrid systems domain is focused on the construction of a unified framework for modeling discrete and continuous systems and on the hard task of developing verification tools for continuous and hybrid systems.