F Nous contacter


0

Documents  68Q60 | enregistrements trouvés : 8

O
     

-A +A

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

P Q

We show that two-player stochastic games with perfect-information and shift-invariant submixing payoff functions are half-positional, i.e. in these games the maximizer has a positional optimal strategy. This extension of our previous result for one-player games relies on an interesting existence result about the existence of epsilon-subgame-perfect strategies.

68Q60 ; 91AXX

Tree Automata Completion is an algorithm computing, or approximating, terms reachable by a term rewriting system. For many classes of term rewriting systems whose set of reachable terms is known to be regular, this algorithm is exact. Besides, the same algorithm can handle **any** left-linear term rewriting system, in an approximated way, using equational 2 abstractions. Thanks to those two properties, we will see that regular languages and tree automata completion provide a promising alternative for automatic static analysis of functional programs. Tree Automata Completion is an algorithm computing, or approximating, terms reachable by a term rewriting system. For many classes of term rewriting systems whose set of reachable terms is known to be regular, this algorithm is exact. Besides, the same algorithm can handle **any** left-linear term rewriting system, in an approximated way, using equational 2 abstractions. Thanks to those two properties, we will see that regular languages and tree ...

68Q60 ; 68Q45

Multi angle  Proof and computation in Coq
Théry, Laurent (Auteur de la Conférence) | CIRM (Editeur )

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

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

Multi angle  Programming with numerical uncertainties
Darulova, Eva (Auteur de la Conférence) | CIRM (Editeur )

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

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

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

Nous confions à nos ordinateurs de nombreux calculs mais la machine a des limites due à son arithmétique dite à virgule flottante. D'une part chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux. D'autre part, les valeurs que l'ordinateur appréhende ont des limites vers l'infiniment petit et l'infiniment grand. Hors de ces bornes, l'ordinateur produit des valeurs spéciales souvent inattendues. La première partie de cet exposé montrera que l'ordinateur n'est pas infaillible ou plutôt que son utilisation est parfois abusive. La seconde partie consisitera en une utilisation judicieuse de l'arithmétique flottante de façon à récupérer les erreurs ou à garantir un calcul
presque juste, même dans les cas pathologiques.
Nous confions à nos ordinateurs de nombreux calculs mais la machine a des limites due à son arithmétique dite à virgule flottante. D'une part chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux. D'autre part, les valeurs que l'ordinateur appréhende ...

65G50 ; 68T15 ; 65G20 ; 68Q60 ; 65Y04

Nuage de mots clefs ici

Z