Raisonnement Assisté Par Ordinateur: Une Approche

Matt Kaufmann, Panagiotis Manolios et J Strother Moore, Kluwer Academic Publishers, Juin 2000. (ISBN 0-7923-7744-3)

  • La Description
  • Table des matières et extraits (pdf .2Mb) (ps .8Mb).
  • Annexes (« Utilisation du Système ACL2 », « Fonctions Supplémentaires »), Bibliographie et Index (pdf)
  • Errata
  • Solutions aux Exercices
  • Informations de Commande

La Description

Ce livre est une introduction au raisonnement assisté par ordinateur. Il peut être utilisé dans les cours de premier cycle des cycles supérieurs et supérieurs sur le génie logiciel ou les méthodes formelles. Il convient également en conjonction avec d’autres livres dans des cours sur la conception matérielle, les mathématiques discrètes ou la théorie, en particulier les cours mettant l’accent sur le formalisme, la rigueur ou le support mécanisé. Il convient également aux cours sur l’Intelligence Artificielle ou le Raisonnement Automatisé.

Les systèmes matériels et logiciels actuels sont souvent très complexes et la tendance va vers une complexité accrue. En modélisant les systèmes mathématiquement, nous obtenons des modèles dont nous pouvons prouver qu’ils se comportent correctement. Pour accroître encore la confiance dans notre raisonnement, qui peut être complexe, nous pouvons utiliser un programme informatique pour vérifier nos épreuves et même pour automatiser une partie de leur construction.

Dans ce livre, nous présentons:

  • Un langage de programmation fonctionnel fonctionnel étroitement lié au Common Lisp qui est utilisé pour définir des fonctions (qui peuvent modéliser des systèmes informatiques) et pour faire des affirmations sur des fonctions définies.
  • Une logique formelle dans laquelle les fonctions définies correspondent aux axiomes; la logique est de premier ordre, inclut l’induction et permet de prouver des théorèmes sur les fonctions.
  • Le système de raisonnement assisté par ordinateur ACL2, qui comprend le langage de programmation, la logique et le support mécanique pour le processus de preuve.

Ce livre vous apprendra comment formaliser les choses, comment construire des preuves et comment utiliser un outil mécanique pour vérifier ces preuves.

Nous utilisons un formalisme particulier et une mécanisation particulière de celui-ci, à savoir ACL2, qui est disponible gratuitement sous les termes d’une licence de type BSD à partir de la page d’accueil ACL2. ACL2 a été écrit par Kaufmann et Moore et est le successeur du «  prouveur de théorème de Boyer-Moore  », Nqthm. (Bob Boyer a également apporté d’importantes contributions préliminaires à ACL2.) La page d’accueil d’ACL2 comprend le manuel de référence en ligne, qui est un grand document hypertexte destiné principalement aux utilisateurs du système. Ce livre est l’introduction définitive à ACL2 et comment l’utiliser.

Tout en enseignant l’utilisation du formalisme mécanisé, nous nous concentrons sur les problèmes de calcul du type généralement rencontré par une personne utilisant des méthodes formelles pour analyser du matériel informatique ou des logiciels.

ACL2 est utilisé dans l’industrie. Rappelez-vous le bogue Intel FDIV? Le premier Pentium [marque déposée, Intel, Inc] n’a pas pu diviser correctement les nombres à virgule flottante et il aurait coûté 500 millions de dollars à Intel pour le réparer. Au moment où cela se produisait, nous avons utilisé ACL2 pour vérifier que le microcode à division en virgule flottante sur le microprocesseur concurrent d’AMD, l’AMD-K5, était correct. AMD a utilisé ACL2 pour vérifier les opérations élémentaires en virgule flottante pour l’Athlon récemment publié. [Remarque: AMD, le logo AMD et leurs combinaisons, AMD-K5, AMD-K7 et AMD Athlon sont des marques commerciales d’Advanced Micro Devices, Inc.] Le volume compagnon présente une étude de cas étroitement liée.

Le système ACL2 a été appliqué avec succès à des projets d’intérêt commercial, y compris la modélisation de microprocesseurs, la vérification du matériel, la vérification des microcodes et la vérification des logiciels. Ce livre donne une méthodologie pour la modélisation formelle des systèmes informatiques et pour raisonner sur ces modèles avec une assistance mécanisée. Le caractère pratique du raisonnement assisté par ordinateur est davantage démontré dans le livre d’accompagnement, Raisonnement Assisté par Ordinateur: Études de Cas ACL2.


Laisser un commentaire

Votre adresse de messagerie ne sera pas publiée. Les champs obligatoires sont indiqués avec *