Severité : 8192
Message : Call-time pass-by-reference has been deprecated
Fichier : controllers/plateformes.php
N° Ligne : 64
Retour Ă l'index des plateformes
|
|
|
 Benjamin Monate Tel. : 01 69 08 94 09 relation.entreprises@cea.fr www.cea.fr |
La vérification du bon fonctionnement d'un logiciel est un enjeu industriel majeur. L'analyse formelle du code source d'un logiciel et de ses propriétés (erreurs, ressources nécessaires, temps d'exécution, contrats fonctionnels...) est une activité économiquement et techniquement réaliste. Frama-C, issue d'un travail commun entre le CEA LIST et l'INRIA, est une plateforme logicielle ouverte permettant la collaboration de modules d'analyse de code source. Elle fournit une représentation du programme à analyser et une manière d'y attacher des propriétés démontrées ou à démontrer. De nombreuses extensions sont fournies pour aider à prouver ces propriétés. L'objectif est de populariser Frama-C pour que les utilisateurs potentiels se familiarisent avec les possibilités offertes par ce type d'outil et que les fournisseurs de technologie ajoutent d'autres extensions, ouvertes ou propriétaires, afin d'élargir l'offre.
http://frama-c.cea.fr
