m

F Nous contacter

0

Documents  68N30 | enregistrements trouvés : 17

O
     

-A +A

P Q

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- xvi; 486 p.
ISBN 978-3-03719-186-6

EMS series of congress reports

Localisation : Colloque 1er étage (TRON)

analyse infinitésimale # équation aux dérivées partielles # loi de conservation hyperbolique # analyse stochastique # théorie spectrale # évolution discrète # système complètement intégrable # matrice aléatoire # dynamique chaotique

15B52 ; 35J10 ; 35L65 ; 35Q41 ; 35Q51 ; 35Q53 ; 37K10 ; 42B20 ; 46N20 ; 46N30 ; 46T12 ; 47B36 ; 47F05 ; 60H20 ; 68N30 ; 76S05 ; 33C45 ; 35A01 ; 35A02 ; 35L80 ; 37D45 ; 39A12 ; 47A10 ; 47N20 ; 47N30 ; 60B20

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- 421 p.
ISBN 978-3-540-70593-2

Lecture notes in computer science , 5133

Localisation : Collection 1er étage

méthodologie de programmation # calcul formel # précision # concision # spécification # langage sémantique

68Q55 ; 68Q60 ; 68N30

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- 552p.
ISBN 978-3-540-67282-1

Lecture notes in computer science , 1785

Localisation : Collection 1er étage

informatique # logique de programmation # softwere pour ingénieurs # algorithme de spécification # algorithme de vérification # algorithme d'analyse # algorithme de construction # algorithme de démonstration de théorème

00B25 ; 68-06 ; 68M14 ; 68Q85 ; 68W15 ; 68N30

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- 443p.
ISBN 978-3-540-65703-3

Lecture notes in computer science , 1579

Localisation : Collection 1er étage

informatique # logique de programmation # softwere pour ingénieurs # algorithme de spécification # algorithme de vérification # algorithme d'analyse # algorithme de construction # algorithme de démonstration de théorème

00B25 ; 68-06 ; 68M14 ; 68Q85 ; 68W15 ; 68N30

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- 431p.
ISBN 978-3-540-62790-6

Lecture notes in computer science , 1217

Localisation : Collection 1er étage

informatique # logique de programmation # softwere pour ingénieurs # algorithme de spécification # algorithme de vérification # algorithme d'analyse # algorithme de construction # algorithme de démonstration de théorème

00B25 ; 68-06 ; 68M14 ; 68Q85 ; 68W15 ; 68N30

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- 434p.
ISBN 978-3-540-61042-7

Lecture notes in computer science , 1055

Localisation : Collection 1er étage

informatique # logique de programmation # softwere pour ingénieurs # algorithme de spécification # algorithme de vérification # algorithme d'analyse # algorithme de construction # algorithme de démonstration de théorème

00B25 ; 68-06 ; 68M14 ; 68N30 ; 68Q85 ; 68W15

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- 289p.
ISBN 978-3-540-60630-7

Lecture notes in computer science , 1019

Localisation : Collection 1er étage

informatique # logique de programmation # softwere pour ingénieurs # algorithme de spécification # algorithme de vérification # algorithme d'analyse # algorithme de construction # algorithme de démonstration de théorème

00B25 ; 68-06 ; 68M14 ; 68Q85 ; 68W15 ; 68N30

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- 422p.
ISBN 978-3-540-56496-6

, 0663

Localisation : Collection 1er étage

informatique # méthode de vérification assistée par ordinateur # simulation numérique # logique pour programmation # softwere pour ingénieurs # calcul parallèle

00B25 ; 68-06 ; 68N30

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- 504p.
ISBN 978-3-540-56922-0

Lecture notes in computer science , 0697

Localisation : Collection 1er étage

informatique # vérification assistée par ordinateur # simulation nummérique # logique de programmation # softwere pour ingénieurs # algorithme de démonstration de théorème # symmetrie

00B25 ; 68-06 ; 68T15 ; 68N30 ; 68Q60

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

Research talks;Computer Science

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

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

Research talks;Computer Science

Numerical software, common in scientific computing or embedded systems, inevitably uses an approximation of the real arithmetic in which most algorithms are designed. Finite-precision arithmetic, such as fixed-point or floating-point, is a common and efficient choice, but introduces an uncertainty on the computed result that is often very hard to quantify. We need adequate tools to estimate the errors introduced in order to choose suitable approximations which satisfy the accuracy requirements.
I will present a new programming model where the scientist writes his or her numerical program in a real-valued specification language with explicit error annotations. It is then the task of our verifying compiler to select a suitable floating-point or fixed-point data type which guarantees the needed accuracy. I will show how a combination of SMT theorem proving, interval and affine arithmetic and function derivatives yields an accurate, sound and automated error estimation which can handle nonlinearity, discontinuities and certain classes of loops.
Additionally, finite-precision arithmetic is not associative so that different, but mathematically equivalent, orders of computation often result in different magnitudes of errors. We have used this fact to not only verify but actively improve the accuracy by combining genetic programming with our error computation with encouraging results.
Numerical software, common in scientific computing or embedded systems, inevitably uses an approximation of the real arithmetic in which most algorithms are designed. Finite-precision arithmetic, such as fixed-point or floating-point, is a common and efficient choice, but introduces an uncertainty on the computed result that is often very hard to quantify. We need adequate tools to estimate the errors introduced in order to choose suitable ...

68Q60 ; 65G50 ; 68N30 ; 68T20

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

Research talks;Computer Science

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

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

Research talks;Computer Science

In this talk, we are going to show on some elementary examples how computation can easily be incorporated inside proof in a proof system like Coq.

68N30 ; 68Q60 ; 68T15

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- xxi; 466 p.
ISBN 978-1-4471-6484-5

Springer monographs in mathematics

Localisation : Ouvrage RdC (LOWE)

distribution # analyse fonctionnelle # espace topologique # espace de jauge # indice

06B35 ; 18B30 ; 18B99 ; 46A19 ; 46B04 ; 46M15 ; 54A05 ; 54B20 ; 54B30 ; 54D30 ; 54D35 ; 54E35 ; 54E99 ; 60B10 ; 60F05 ; 68N30 ; 68Q99 ; 54-02

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- xxiii; 572 p.
ISBN 978-0-8176-4704-9

Localisation : Ouvrage RdC (HAND)

Arithmétique à virgule flottante # langage de programmation # nombre à virgule flottante # algorithme # implémentation logicielle # implémentation matérielle # compilateur

65Y99 ; 68N30 ; 65-01 ; 68M07 ; 68N20 ; 68N15

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- xii; 343 p.
ISBN 978-3-540-33258-9

Mathematics and visualization

Localisation : Ouvrage RdC (EFFE)

graphisme # informatique # géométrie calculatoire non-linéaire # structure de données # algorithme # courbe # surface # topologie calculatoire

68U05 ; 65D18 ; 14Q05 ; 14Q10 ; 14Q20 ; 68N19 ; 68N30 ; 65D17 ; 57Q15 ; 57R05 ; 57Q55 ; 65D05 ; 57N05 ; 57N65 ; 58A05 ; 68W05 ; 68W20 ; 68W25 ; 68W40 ; 68W30 ; 33F05 ; 57N25 ; 58A10 ; 58A20 ; 58A25 ; 65-06 ; 00B15

... Lire [+]

Déposez votre fichier ici pour le déplacer vers cet enregistrement.

- 420 p.
ISBN 978-0-387-23759-6

Monographs in computer science

Localisation : Ouvrage RdC (POER)

aspects mathématiques du software # programmation # logique mathématique # données abstraites # algèbre de spécification # démonstrateur de théorème

03B15 ; 68N18 ; 68Q65 ; 03B20 ; 68N30 ; 68T15 ; 68-02

... Lire [+]

Z