11 résultats : preuve de programme

Pourquoi mon ordinateur calcule faux?

Pourquoi mon ordinateur calcule faux?

Description : Dans cet exposé Sylvie Boldo nous fait prendre conscience de l'importance des bugs en informatique et des conséquences historiques qu'ils ont pu engendrer. Elle se concentre ensuite sur les problèmes liés aux calculs numériques et montre de manière détaillée et constructive comment prendre la mesure ...

Mots clés : bug, algorithmique, arithmétique flottante, calcul informatique, méthode formelle, nombre à virgule flottante, preuve de programme, vérification de logiciel

Date : 16-06-2009

Droits : Droits réservés à l'éditeur et aux auteurs.

Les nombres et l'ordinateur

Les nombres et l'ordinateur

Description : Nous confions à nos ordinateurs de nombreux calculs (météo, simulations aéronautiques, jeux vidéos, feuilles Excel...) et nous considérons naturellement que l'ordinateur fournira une réponse juste. Malheureusement, la machine a ses limites que l'esprit humain n'a pas. Elle utilise une ar ...

Mots clés : calcul informatique, preuve de programme, analyse numérique, arithmétique virgule flottante, erreur de calcul, méthodes formelles

Date : 05-06-2013

Droits : Droits réservés à l'éditeur et aux auteurs.

Demandez le programme

Description : La programmation consiste à décomposer un algorithme en ordres simples et à les écrire en un langage compréhensible par l’ordinateur.

Mots clés : bug, paradigme de programmation, niveau d'abstraction, erreur, preuve de programme, fuscia

Date : 28-11-2008

Droits : Ce document est diffusé sous licence Creative Common : Paternité - Pas d'utilisation commerciale - Pas de modification. http://creativecommons.org/licenses/by-nc-nd/2.0/fr/legalcode

Demandez le programme

Du rêve à la réalité des preuves

Du rêve à la réalité des preuves

Description : Les ordinateurs ne savent pas prouver seuls des théorèmes profonds. Cependant, grâce aux assistants de preuve, ils garantissent les démonstrations découvertes par les mathématiciens.

Mots clés : assistant de preuve, preuve formelle, preuve de programme, logique mathématique, démonstration, complexité, fuscia

Date : 01-08-2011

Droits : Ce document est diffusé sous licence Creative Common : Paternité - Pas d'utilisation commerciale - Pas de modification. http://creativecommons.org/licenses/by-nc-nd/2.0/fr/legalcode

Les ingrédients des algorithmes

Les ingrédients des algorithmes

Description : Pour programmer un ordinateur, le plus important ce sont les méthodes mises en œuvre. Découvrez les ingrédients à combiner pour créer ces algorithmes !

Mots clés : algorithme, programme, séquence d'instructions, boucle, condition, variable, fonction, langage de programmation, erreur, preuve de programme, indécidabilité algorithmique, syntaxe d'un programme, sémantique d'un programme, fuscia

Date : 05-02-2009

Droits : Ce document est diffusé sous licence Creative Common : Paternité - Pas d'utilisation commerciale - Pas de modification. http://creativecommons.org/licenses/by-nc-nd/2.0/fr/legalcode

Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 1ère partie

Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 1ère partie

Description : Nous présentons les systèmes embarqués critiques et les exigences qui leur sont liées : dans certains cas (nucléaire, avionique, santé) aucun bug n'est accepté. Puis nous présentons l'analyse statique, que nous illustrons sur un exemple de programme. Nous montrons que pour analyser des variables ...

Mots clés : algorithmique, treillis de Galois, preuve de programme, analyse de programme, sémantique programmation, génie logiciel

Date : 18-01-2012

Droits : Droits réservés à l'éditeur et aux auteurs. Document libre, dans le cadre de la licence Creative Commons (http://creativecommons.org/licenses/by-nd/2.0/fr/), citation de l'auteur obligatoire et interdiction de désassembler (paternité, pas de modification)

Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 2ème partie

Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 2ème partie

Mots clés : algorithmique, treillis de Galois, preuve de programme, analyse de programme, sémantique programmation, génie logiciel

Date : 18-01-2012

Proofs assistants : from symbolic logic to real mathematics

Proofs assistants : from symbolic logic to real mathematics

Description : Mathematicians have always been prone to error. As proofs get longer and more complicated, the question of correctness looms ever larger. Andrew Wiles’ proof of Fermat’s last theorem contained a flaw that was only fixed a year later. Meanwhile, proof assistants — formal tools originally developed ...

Mots clés : preuve de programme

Date : 18-05-2017

Droits : Droits réservés à l'éditeur et aux auteurs.

Approches fonctionnelles de la programmation

Approches fonctionnelles de la programmation

Description : Fournir un panorama complet du paradigme de programmation fonctionnelle et de son positionnement par rapport aux autres paradigmes de programmation (en particulier de la programmation impérative). Illustrer l'ensemble des concepts abordés au moyen de deux langages fonctionnels: Lisp et Haskell.

Mots clés : fuscia, Lisp, Haskell, preuve de programme

Date : 07-01-2009

Droits : Document libre, dans le cadre de la licence Creative Commons (http://creativecommons.org/licenses/by-nd/2.0/fr/), citation de l'auteur obligatoire et interdiction de désassembler (paternité, pas de modification)