F Nous contacter


0

Documents  68N15 | enregistrements trouvés : 6

O
     

-A +A

Sélection courante (0) : Tout sélectionner / Tout déselectionner

P Q

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.
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 ...

68N30 ; 68Q60 ; 68N15 ; 65Y04 ; 65G50

This talk is about verified numerical algorithms in Isabelle/HOL, with a focus on guaranteed enclosures for solutions of ODEs. The enclosures are represented by zonotopes, arising from the use of affine arithmetic. Enclosures for solutions of ODEs are computed by set-based variants of the well-known Runge-Kutta methods.
All of the algorithms are formally verified with respect to a formalization of ODEs in Isabelle/HOL: The correctness proofs are carried out for abstract algorithms, which are specified in terms of real numbers and sets. These abstract algorithms are automatically refined towards executable specifications based on lists, zonotopes, and software floating point numbers. Optimizations for low-dimensional, nonlinear dynamics allow for an application highlight: the computation of an accurate enclosure for the Lorenz attractor. This contributes to an important proof that originally relied on non-verified numerical computations.
This talk is about verified numerical algorithms in Isabelle/HOL, with a focus on guaranteed enclosures for solutions of ODEs. The enclosures are represented by zonotopes, arising from the use of affine arithmetic. Enclosures for solutions of ODEs are computed by set-based variants of the well-known Runge-Kutta methods.
All of the algorithms are formally verified with respect to a formalization of ODEs in Isabelle/HOL: The correctness proofs are ...

68T15 ; 34-04 ; 34A12 ; 37D45 ; 65G20 ; 65G30 ; 65G50 ; 65L70 ; 68N15 ; 68Q60 ; 68N30 ; 65Y04

Cet exposé présente un certain nombre d'exemples d'exercices de programmation sur les arbres qui peuvent être effectués dans les premières années d'université. Les programmes étant eux-mêmes des arbres, écrire des programmes qui opèrent sur des arbres permet d'écrire des programmes qui opèrent sur d'autres programmes.

68Wxx ; 68N15

Explication de ce qu'est un buffer overflow, de la façon de l'exploiter, des protections possibles et des contournements...

68M10 ; 68N15 ; 68P25 ; 68Q60

Multi angle  L'importance des langages en informatique
Berry, Gérard (Auteur de la Conférence) | CIRM (Editeur )

Nuage de mots clefs ici

Z