34 résultats : preuves

Attention : l'accès aux ressources peut être restreint, soit pour des raisons juridiques, soit par la volonté de l'auteur.
34 résultats
page 1.0 sur 2
résultats -9 à 15
UNIT
L’informatisation des objets, ou l’invasion des pucerons
Description : Les systèmes embarqués envahissent tous les pans de l’industrie, depuis l’avionique jusqu’aux objets de la vie courante. Doit-on redouter cette évolution technologique ? Regardez cette conférence de Gérard Berry...
Mots clés : informatisation, bug application, preuve formelle, circuit, fuscia
Date : 08-06-2006
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
 En savoir plus
 Description complète
L’informatisation des objets, ou l’invasion des pucerons
 Ajouter à mon panier
Accéder au document
Droits d'accès : non autorisé
UNIT
Preuves de programmes en coq
Description : Le système Coq fournit un langage de programmation symbolique et un cadre logique pour raisonner sur les algorithmes décrits. Dans ce cours, nous décrivons les points clefs du langage de programmation, basé sur la programmation fonctionnelle, et du cadre logique de vérification, basé sur la logique ...
Mots clés : Coq, assistant de preuve, programmation fonctionnelle sûre, preuve de programme, logique mathématique, méthode formelle, calcul des constructions, correction de logiciel, algorithmique certifiée, théorie des types, logiciel libre, récursion, fuscia
Date : 21-09-2012
Droits : Ces ressources de cours sont la copropriété, à parts égales, d’UNIT et de l'Inria et relèvent de la licence logicielle GPL, dans sa version française CeCILL : http://www.cecill.info/licences/Licence_CeCILL-V1_VF.pdf
 En savoir plus
 Description complète
Preuves de programmes en coq
 Supprimer de mon panier
Accéder au document
Droits d'accès : non autorisé
Canal-U
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.
 En savoir plus
 Description complète
Pourquoi mon ordinateur calcule faux?
 Ajouter à mon panier
Accéder aux documents
Canal-U
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.
 En savoir plus
 Description complète
Les nombres et l'ordinateur
 Ajouter à mon panier
Accéder aux documents
UNIT
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
 En savoir plus
 Description complète
Demandez le programme
 Ajouter à mon panier
Accéder au document
Droits d'accès : non autorisé
Canal-U
Les dynamiques d'introduction et de réception des recommandations en médecine
Description : Deuxième volet de la collection « Les formes de la médecine contemporaine ». La situation de la médecine contemporaine apparaît, à bien des égards, paradoxale. Elle occupe en effet une position éminente dans le monde contemporain et se voit amener à prendre en charge un nombre toujours plus grand ...
Mots clés : sociologie, aléas, connaissance, evidence based medicine, judiciarisation, médecine fondée sur les preuves, normes de pratiques, plasticité des normes, pratiques locales, réflexivité, relation thérapeutique, relation médecin-patient, recommandation, qualité, normalisation, médecine, coordination, ...
Date : 30-10-2009
Droits : Droits réservés à l'éditeur et aux auteurs.
 En savoir plus
 Description complète
Les dynamiques d'introduction et de réception des recommandations en médecine
 Ajouter à mon panier
Accéder aux documents
UNIT
Une preuve sur les nombres premiers
Description : Un ordinateur, c’est avant tout une machine. Est-il alors bien raisonnable de lui confier des démonstrations ? Voici un exemple propre à convaincre les sceptiques.
Mots clés : algorithme de Knuth, preuve formelle, Coq, complexité, fuscia
Date : 24-02-2004
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
 En savoir plus
 Description complète
Une preuve sur les nombres premiers
 Ajouter à mon panier
Accéder au document
Droits d'accès : non autorisé
Canal-U
RMJCA N9 - Vérité et preuve scientifique
Description : Le professeur Jacques COHEN, nous explique quelle est l'utilité de preuves scientifiques pour prouver la vérité.
Mots clés : Faculté de Médecine de Reims, Manifestation de la Vérité, preuve, scientifique
Date : 15-05-2009
Droits : Droits réservés à l'éditeur et aux auteurs.
 En savoir plus
 Description complète
RMJCA N9 - Vérité et preuve scientifique
 Ajouter à mon panier
Accéder aux documents
Canal-U
Formation à la lecture critique d'articles : Introduction à la LCA 1/3
Description : La médecine fondée sur les faits (MFF) repose sur l’utilisation pertinente, dans la pratique quotidienne du médecin et du personnel soignant, des meilleures données disponibles issues d’études cliniques de qualité. La MFF nécessite donc pour partie, de la part des soignants, une capacité à lire ...
Mots clés : maladie d'Alzheimer, pédagogie médicale, evidence-based medecine, jugement clinique, lecture critique d'articles (LCA), littérature scientifique (analyse critique), médecine (prise de décision), médecine fondée sur la preuve
Date : 23-09-2009
Droits : Droits réservés à l'éditeur et aux auteurs.
 En savoir plus
 Description complète
Formation à la lecture critique d'articles : Introduction à la LCA 1/3
 Ajouter à mon panier
Accéder aux documents
Canal-U
Formation à la lecture critique d'articles : Analyse de la publication d’un essai thérapeutique 2/3
Description : La médecine fondée sur les faits (MFF) repose sur l’utilisation pertinente, dans la pratique quotidienne du médecin et du personnel soignant, des meilleures données disponibles issues d’études cliniques de qualité. La MFF nécessite donc pour partie, de la part des soignants, une capacité à lire ...
Mots clés : maladie d'Alzheimer, pédagogie médicale, evidence-based medecine, jugement clinique, lecture critique d'articles (LCA), littérature scientifique (analyse critique), médecine (prise de décision), médecine fondée sur la preuve
Date : 23-09-2009
Droits : Droits réservés à l'éditeur et aux auteurs.
 En savoir plus
 Description complète
Formation à la lecture critique d'articles : Analyse de la publication d’un essai thérapeutique 2/3
 Ajouter à mon panier
Accéder aux documents
Canal-U
Formation à la lecture critique d'articles : Analyse de la publication d’une étude pronostique 3/3
Description : La médecine fondée sur les faits (MFF) repose sur l’utilisation pertinente, dans la pratique quotidienne du médecin et du personnel soignant, des meilleures données disponibles issues d’études cliniques de qualité. La MFF nécessite donc pour partie, de la part des soignants, une capacité à lire ...
Mots clés : maladie d'Alzheimer, pédagogie médicale, evidence-based medecine, jugement clinique, lecture critique d'articles (LCA), littérature scientifique (analyse critique), médecine (prise de décision), médecine fondée sur la preuve
Date : 23-09-2009
Droits : Droits réservés à l'éditeur et aux auteurs.
 En savoir plus
 Description complète
Formation à la lecture critique d'articles : Analyse de la publication d’une étude pronostique 3/3
 Ajouter à mon panier
Accéder aux documents
UNIT
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
 En savoir plus
 Description complète
Du rêve à la réalité des preuves
 Ajouter à mon panier
Accéder au document
Droits d'accès : non autorisé
UNIT
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
 En savoir plus
 Description complète
Les ingrédients des algorithmes
 Ajouter à mon panier
Accéder au document
Droits d'accès : non autorisé
Canal-U
HIT Paris 2007 ? EBM, aide à la décision, assurer l'accès aux connaissances dans les systèmes d'information médicaux.
Description : Les professionnels ne trouvent pas en situation l'information dont ils ont besoin. le surcoût lié aux erreurs dans la prescription médicamenteuse est énorme , près de 2000 à 2600 US dollars par séjour. L'aide à la décision permet donc de réduire les coûts et d'améliorer la démarche qualité. Les ...
Mots clés : qualité, HIT, coûts, aide à la décision, EBM, médecine par la preuve, prescription médicamenteuse
Date : 24-05-2007
Droits : Droits réservés à l'éditeur et aux auteurs.
 En savoir plus
 Description complète
HIT Paris 2007 ? EBM, aide à la décision, assurer l'accès aux connaissances dans les systèmes d'information médicaux.
 Ajouter à mon panier
Accéder aux documents
Canal-U
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)
 En savoir plus
 Description complète
Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 1ère partie
 Ajouter à mon panier
Accéder aux documents
Canal-U
Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 2ème 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)
 En savoir plus
 Description complète
Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 2ème partie
 Ajouter à mon panier
Accéder aux documents
Canal-U
Témoignage et vérité scientifique. Le cas des météorites / Matthieu Gounelle
Description : Témoignage et vérité scientifique. Le cas des météorites / Matthieu Gounelle. In "La Vérité", Journées Scientifiques annuelles de l'Institut Universitaire de France, organisées par le Pôle de recherche et d'enseignement supérieur (PRES) de Toulouse, l'Université Toulouse II-Le Mirail et l'Institut ...
Mots clés : météorite, connaissance scientifique, témoignage, vérité (épistémologie), preuve (épistémologie)
Date : 02-04-2013
Droits : Droits réservés à l'éditeur et aux auteurs. Tous droits réservés à l'Université Toulouse II-Le Mirail et aux auteurs.
 En savoir plus
 Description complète
Témoignage et vérité scientifique. Le cas des météorites / Matthieu Gounelle
 Ajouter à mon panier
Accéder aux documents
Canal-U
La vérité : conclusion / Olivier Guerrier
Description : La vérité : conclusion / Olivier Guerrier. In "La vérité", Journées Scientifiques annuelles de l'Institut Universitaire de France, organisées par le Pôle de recherche et d'enseignement supérieur (PRES) de Toulouse, l'Université Toulouse II-Le Mirail et l'Institut Universitaire de France. Toulouse ...
Mots clés : connaissance scientifique, objectivité, vérité (épistémologie), relation pouvoir-vérité, preuve (épistémologie)
Date : 04-04-2013
Droits : Droits réservés à l'éditeur et aux auteurs. Tous droits réservés à l'Université Toulouse II-Le Mirail et aux auteurs.
 En savoir plus
 Description complète
La vérité : conclusion / Olivier Guerrier
 Ajouter à mon panier
Accéder aux documents
UNIT
Règles de déduction sur les connecteurs
Description : Ce cours est le deuxième d'une série de 5 cours de l'enseignement de logique du cursus de Licence Informatique de Sorbonne Universités. Il présente un ensemble de règles de déduction sur les connecteurs logiques permettant de prouver des formules
Mots clés : langage logique, représentation des preuves, axiome, règle d'affaiblissement, connecteur, logique classique, raisonnement par l'absurde
Date : 10-01-2020
Droits : Attribution - Partage dans les mêmes conditions (CC BY-SA)
 En savoir plus
 Description complète
Règles de déduction sur les connecteurs
 Ajouter à mon panier
Accéder au document
Droits d'accès : non autorisé
Canal-U
SIFEM 2009 - Comment enseigner la Médecine fondée sur les preuves lors des stages cliniques ?
Description : Titre : Comment enseigner la Médecine fondée sur les preuves lors des stages cliniques ? L’étudiant en médecine et la médecine fondée sur les preuves. Résumé : Médecine fondée sur les preuves : « Utilisation consciencieuse, explicite et judicieuse de la meilleure preuve pour décider des soins ap ...
Mots clés : Formation, médecine, diagnostic, recommandations, patient, preuves, pratique clinique, SIFEM 2009, dossier clinique
Date : 26-10-2009
Droits : Droits réservés à l'éditeur et aux auteurs.
 En savoir plus
 Description complète
SIFEM 2009 - Comment enseigner la Médecine fondée sur les preuves lors des stages cliniques ?
 Ajouter à mon panier
Accéder aux documents
UNIT
Comment faire confiance à un compilateur ? (série : Colloquium Jacques Morgenstern)
Description : Les outils de vérification formelle de programmes (analyseurs statiques, prouveurs de programmes, model-checkers) ont fait des progrès remarquables ces dernières années et commencent à percer dans le monde du logiciel critique. Cependant, ces outils ne vérifient "que" des programmes source: des ...
Mots clés : compilateur, logiciel critique, programmation fonctionnelle, vérification de programme, vérification formelle, preuve formelle, fuscia, conference, stic, recherche
Date : 08-10-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)
 En savoir plus
 Description complète
Comment faire confiance à un compilateur ? (série : Colloquium Jacques Morgenstern)
 Ajouter à mon panier
Accéder au document
Droits d'accès : non autorisé
UNIT
Comment faire confiance à un compilateur ?
Description : Comment faire exécuter par une machine des programmes écrits dans un langage de haut niveau, qu’elle ne peut comprendre ?
Mots clés : erreur, langage haut niveau, fossé sémantique, preuve formelle, CompCert, fuscia
Date : 30-03-2010
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
 En savoir plus
 Description complète
Comment faire confiance à un compilateur ?
 Ajouter à mon panier
Accéder au document
Droits d'accès : non autorisé
Canal-U
Vérités, bibliométrie et catastrophisme en géoarchéologie littorale : un déterminisme dangereux ? / Christophe Morhange
Description : Vérités, bibliométrie et catastrophisme en géoarchéologie littorale : un déterminisme dangereux ? / Christophe Morhange. In "La vérité", Journées Scientifiques annuelles de l'Institut Universitaire de France, organisées par le Pôle de recherche et d'enseignement supérieur (PRES) de Toulouse, l'U ...
Mots clés : catastrophe naturelle, géomorphologie, paléoenvironnement, connaissance scientifique, causalité, Environnement et risques, archéologie littorale, preuve (épistémologie)
Date : 03-04-2013
Droits : Droits réservés à l'éditeur et aux auteurs. Tous droits réservés à l'Université Toulouse II-Le Mirail et aux auteurs.
 En savoir plus
 Description complète
Vérités, bibliométrie et catastrophisme en géoarchéologie littorale : un déterminisme dangereux ? / Christophe Morhange
 Ajouter à mon panier
Accéder aux documents
UNIT
Les leçons d’un algorithme délinquant
Description : Pour le sens commun, la machine ne se trompe jamais. Si par malheur un utilisateur pointilleux découvre une erreur dans son calcul sur ordinateur, qui doit-il alors accuser ? Lui, ou la machine ?
Mots clés : bug, Pentium, implémentation d'algorithmes, erreur, preuve formelle, fuscia
Date : 19-02-2004
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
 En savoir plus
 Description complète
Les leçons d’un algorithme délinquant
 Ajouter à mon panier
Accéder au document
Droits d'accès : non autorisé
Canal-U
RMJCA N6 - De la scène de crime à la preuve génétique - IFEG
Description : Le docteur Olivier PASCAL, Président de l'Institut Français des Empreintes Génétiques (IFEG) et Monsieur Eric TABARY Directeur de l'IFEG, montrent quelle est l'utilité des empreintes génétiques en tant que preuve.
Mots clés : ADN, preuves, Faculté de Médecine de Reims, Manifestation de la Vérité
Date : 15-05-2009
Droits : Droits réservés à l'éditeur et aux auteurs.
 En savoir plus
 Description complète
RMJCA N6 - De la scène de crime à la preuve génétique - IFEG
 Ajouter à mon panier
Accéder aux documents