Il y a 4 Résultats avec le mot clé : "vérification"

FRAMAC

Showroom des démos

Frama-C, une boîte à outils pour la vérification de logiciels en C

Frama-C fait collaborer de nombreuses techniques d'analyse statique, de la vérification de règles de codage à l'analyse par interprétation abstraite et la vérification de spécifications fonctionnelles grâce aux principes de l’approche déductive de la vérification de programmes. Les domaines visés sont le logiciel embarqué critique, les implémentations de bibliothèques cryptographiques, et la sécurité.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Aéronautique, défense, spatial, sécurité > Démos > Frama-C, une boîte à outils pour la vérification de logiciels en C

Lire la suite

Showroom des démos

Astrée : Preuve d'Absence d'Erreurs à l'Exécution

Astrée est un analyseur statique permettant la preuve d'absence d'erreurs à l'exécution dans des programmes C critiques embarqués. Cette preuve est entièrement automatique, et est effectuée au niveau du code source, vis à vis de la sémantique du langage. Astrée a analysé avec succès des applications de taille industrielle dans le domaine aéronautique et spatial. L'analyseur Astrée a été conçu et développé au sein de l'équipe Abstraction. Il est actuellement diffusé par l'entreprise Absint Angewandte Informatik.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Aéronautique, défense, spatial, sécurité > Démos > Astrée : Preuve d'Absence d'Erreurs à l'Exécution

Lire la suite

Showroom des démos

Astrée : Preuve d'Absence d'Erreurs à l'Exécution

Astrée est un analyseur statique permettant la preuve d'absence d'erreurs à l'exécution dans des programmes C critiques embarqués. Cette preuve est entièrement automatique, et est effectuée au niveau du code source, vis à vis de la sémantique du langage. Astrée a analysé avec succès des applications de taille industrielle dans le domaine aéronautique et spatial. L'analyseur Astrée a été conçu et développé au sein de l'équipe Abstraction. Il est actuellement diffusé par l'entreprise Absint Angewandte Informatik.

Mots-clés :

Accueil > Innovation > Secteurs industriels > Edition de logiciels, systèmes embarqués > Démos > Astrée : Preuve d'Absence d'Erreurs à l'Exécution

Lire la suite

Hubert Garavel - © Inria / Photo A.Eidelman

Distinction

Hubert Garavel, lauréat prix Humboldt

Isabelle Bellin - 16/05/2011

Hubert Garavel, responsable de l'équipe-projet VASY, est le quatrième Français à recevoir le prix scientifique Gay-Lussac Humboldt dans le domaine de l’informatique. Avant lui, Alain Bensoussan, ancien président de l’Inria, avait reçu ce prix en 1983. A l’occasion de ce prix, Hubert Garavel est invité en Allemagne où il sera accueilli par le professeur Holger Hermanns, doyen de la faculté de mathématiques et informatique de l’université de la Sarre, avec lequel il collabore depuis 10 ans.

Mots-clés :

Accueil > Centre > Grenoble > Actualités > Hubert Garavel, lauréat prix Humboldt

Lire la suite

Haut de page

Siège et centres de recherche Inria

Accès direct

Social