Inria
Inria.fr
Inria Channel
Il y a 6 Résultats avec le mot clé : "PROVAL"
Showroom des démos
Alt-Ergo, preuve automatique pour la certification de code critique
Alt-Ergo est un logiciel pour la démonstration automatique de théorèmes. Il est dédié à la preuve déductive de programmes, qui réduit la correction d'un programme par rapport à sa spécification à la validité d'une formule logique. En particulier, Alt-ergo est situé en bout de chaîne de plate-formes de preuve utilisées dans l'avionique. Selon la complexité des codes analysés, ce sont des milliers de formules qu'il faut prouver. Parce qu'il n'est pas envisageable de faire toutes ces preuves à la main, l'utilisation d'un outil comme Alt-Ergo est cruciale pour le passage à l'échelle de cette approche."
Mots-clés :
Accueil > Innovation > Secteurs industriels > Aéronautique, défense, spatial, sécurité > Démos > Alt-Ergo, preuve automatique pour la certification de code critique
Showroom des démos
Alt-Ergo, preuve automatique pour la certification de code critique
Alt-Ergo est un logiciel pour la démonstration automatique de théorèmes. Il est dédié à la preuve déductive de programmes, qui réduit la correction d'un programme par rapport à sa spécification à la validité d'une formule logique. En particulier, Alt-ergo est situé en bout de chaîne de plate-formes de preuve utilisées dans l'avionique. Selon la complexité des codes analysés, ce sont des milliers de formules qu'il faut prouver. Parce qu'il n'est pas envisageable de faire toutes ces preuves à la main, l'utilisation d'un outil comme Alt-Ergo est cruciale pour le passage à l'échelle de cette approche."
Mots-clés :
Accueil > Innovation > Secteurs industriels > Edition de logiciels, systèmes embarqués > Démos > Alt-Ergo, preuve automatique pour la certification de code critique
© Inria Saclay - Île-de-France
Prix scientifique
Best paper award pour trois chercheurs de Proval
Mohamed Iguernelala, Evelyne Contejean et Sylvain Conchon de l'équipe-projet Proval ont reçu le prix EATC (European Association for Theoretical Computer Science) du meilleur papier ETAPs 2011 (European Joint Conferences on Theory and Practice of Software).
Mots-clés :
Accueil > Centre > Saclay > Actualités > Best paper award pour trois chercheurs de Proval
Algorithmique, programmation, logiciels et architectures
Pourquoi mon ordinateur calcule-t-il faux ?
Réaliser des calculs complexes est devenu chose facile avec nos ordinateurs, mais doit-on aveuglément faire confiance aux résultats obtenus par nos machines ? Comment calculent nos ordinateurs ?
Mots-clés :
Accueil > Centre > Saclay > Recherche > Pourquoi mon ordinateur calcule-t-il faux ?
Algorithmique, programmation, logiciels et architectures
C'est la faute à l'ordinateur !
Qui n'a jamais entendu cette phrase ?
Mots-clés :
Accueil > Centre > Saclay > Recherche > C'est la faute à l'ordinateur !
Preuve de programme
La vérification de programmes en compétition
Six équipes sur les 29 en lice sont arrivées en tête de la compétition sur la preuve de programme associée à la conférence VSTTE 2012 (Verified Software : Theories, Tool and Experiments) qui se déroulait les 28 et 29 janvier à Philadelphie. Retour sur la compétition et ses enjeux avec deux de ses organisateurs, Jean-Christophe Filliâtre et Andrei Paskevich, membres du LRI et de l’équipe Proval.
Mots-clés :
Accueil > Centre > Saclay > Actualités > La vérification de programmes en compétition
Centres de recherche Inria
