VERIMAG

Formal methods and tools for safe and secure computing, applications to cyber-physical systems

Computerized systems control many everyday and professional objects, including those that perform critical functions in the transport (automotive, avionics, rail, space), telecommunications, robotics, banking and healthcare sectors, where expectations in terms of safety and security are particularly high.

Verimag’s work aims to produce theoretical and technical tools to meet these expectations with mathematical rigor, on a broad spectrum of problems that may involve circuits, processors, analog or hybrid systems, compilers, security protocols, distributed algorithms, systems integrating AI, particularly in the context of critical systems.

Verimag seeks to maintain a balance between fundamental, experimental and applied research, in particular through long-term, sustained cooperation with industrial and academic partners.

Verimag has contributed and continues to contribute actively to the development of the state of the art in formal methods (model-checking, static analysis, automated or interactive theorem proving), synchronous languages, system modeling, while integrating sustainability and resource-saving issues.

Verimag’s results have numerous industrial applications, notably in tools for the development of critical software and systems.

Verimag (UMR 5104) was created in 1993 as a CNRS/Verilog Unité Mixte from the Spectre team of the LGI laboratory; since 1997, Verimag has been a joint research unit of University Grenoble Alpes (including Grenoble INP - UGA) and CNRS (INS2I).

Verimag plays an important role in teaching at Grenoble Alpes University and Grenoble-INP, and in training doctoral students.

Verimag is a member of the Institut Carnot LSI and of the Labex PERSYVAL-Lab

For more information, you can have a look at the last activity report or the HCERES evaluation.

Keywords: formal methods: model checking, static analysis, automated and interactive theorem proving, logic, modeling, testing - Critical, embedded, cyber-physical systems - Safety and Security - Synchronous Language, Lustre - Compilation, certified compilation - Coq - Temporal analysis - Trusted AI, explainable AI - robustness of learning models - Frugal computing

Verimag
Bâtiment IMAG
Université Grenoble Alpes
150 place du torrent
38401 Saint Martin d’Hères
FRANCE
Phone: +33 4 57 42 22 42
Fax: +33 4 57 42 22 22

Director: David Monniaux