Multi angle

H 1 Formal verification of numerical analysis programs

Auteurs : Boldo, Sylvie (Auteur de la Conférence)
CIRM (Editeur )

    Loading the player...

    Résumé : From a (partial) differential equation to an actual program is a long road. This talk will present the formal verification of all the steps of this journey. This includes the mathematical error due to the numerical scheme (method error), that is usually bounded by pen-and-paper proofs. This also includes round-off errors due to the floating-point computations.
    The running example will be a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. This program is annotated to specify both method error and round-off error, and formally verified using interactive and automatic provers. Some work in progress about the finite element method will also be presented.

    Codes MSC :
    65G50 - Roundoff error
    68N15 - Programming languages
    68Q60 - Specification and verification (program logics, model checking, etc.)
    68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
    65Y04 - Algorithms for computer arithmetic, etc.

      Informations sur la Vidéo

      Langue : Anglais
      Date de publication : 04/02/16
      Date de captation : 12/01/16
      Collection : Research talks ; Computer Science
      Sous collection : Research talks
      Format : MP4
      Durée : 00:57:56
      Domaine : Computer Science
      Audience : Chercheurs ; Doctorants , Post - Doctorants
      Download : https://videos.cirm-math.fr/2016-01-12_Boldo.mp4

    Informations sur la rencontre

    Nom de la rencontre : Effective analysis: foundations, implementations, certification / Analyse effective: fondations, programmation, certification
    Organisateurs de la rencontre : Mahboubi, Assia ; Schuster, Peter ; Spitters, Bas
    Dates : 11/01/16 - 15/01/16
    Année de la rencontre : 2016
    URL Congrès : http://conferences.cirm-math.fr/1508.html

    Citation Data

    DOI : 10.24350/CIRM.V.18915203
    Cite this video as: Boldo, Sylvie (2016). Formal verification of numerical analysis programs. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.18915203
    URI : http://dx.doi.org/10.24350/CIRM.V.18915203

    Voir aussi


Titres de périodiques et e-books électroniques (Depuis le CIRM)

Ressources Electroniques

Books & Print journals

Recherche avancée