Nous utilisons des cookies pour améliorer votre expérience. Pour nous conformer à la nouvelle directive sur la vie privée, nous devons demander votre consentement à l’utilisation de ces cookies. En savoir plus.
Preuves par récurrence avec ensembles couvrants contextuels
Univ Europeenne - EAN : 9783841794901
Édition papier
EAN : 9783841794901
Paru le : 8 mars 2012
69,00 €
65,40 €
Disponible
Pour connaître votre prix et commander, identifiez-vous
Notre engagement qualité
-
Livraison gratuite
en France sans minimum
de commande -
Manquants maintenus
en commande
automatiquement -
Un interlocuteur
unique pour toutes
vos commandes -
Toutes les licences
numériques du marché
au tarif éditeur -
Assistance téléphonique
personalisée sur le
numérique -
Service client
Du Lundi au vendredi
de 9h à 18h
- EAN13 : 9783841794901
- Réf. fournisseur : 5233661
- Editeur : Univ Europeenne
- Date Parution : 8 mars 2012
- Disponibilite : Disponible
- Barème de remise : NS
- Nombre de pages : 200
- Format : H:229 mm L:152 mm E:12 mm
- Poids : 302gr
- Interdit de retour : Retour interdit
- Résumé : Le processus de certification de logiciels est dans la plupart des cas une tâche laborieuse et coûteuse qui nécessite aussi bien des méthodes mathématiques, pour exprimer sans ambiguïté et de façon structurée le comportement attendu du logiciel, que des outils automatiques pour vérifier ses propriétés. Parmi les techniques de preuve, la récurrence est parfaitement adaptée pour raisonner sur des structures de données non-bornées, comme les entiers et les listes, ou des systèmes paramétrés. Cet ouvrage comprend deux parties, l'une théorique, l'autre applicative. La première partie décrit un principe de preuve par récurrence exprimé par un système d'inférence abstrait à l'aide du concept d'ensembles couvrants contextuels. L'approche est suffisamment générale pour représenter la plupart des systèmes d'inférence actuels basés sur la récurrence implicite dont celui du démonstrateur de théorèmes Spike. La deuxième partie présente la première preuve formelle de l'équivalence entre deux algorithmes génériques de conformité du protocole de télécommunications ABR. Spike a permis de vérifier de manière complètement automatique la majorité des 80 lemmes de cette preuve.
