Accueil
Déposer
S'authentifier
S'inscrire
Consulter
Par domaine
Derniers rentrés
Par date de publication/rédaction
Par type de publication
Par collection
ArXiv
Derniers rentrés dans HAL
Rechercher
Recherche simple
Recherche avancée
Recherche par identifiant
Aide
Aide
Bib2Hal
À propos
Services
S'abonner
Exporter une liste de publication
Export raweb
Consulter les laboratoires connus de HAL
HalTools : Bib2Hal
HalTools : créer sa page web
HalTools : gérer ses identitées
version française
english version
inria-00000892, version 1
Voir la fiche détaillée
BibTeX
EndNote
TEI
RefWorks
%% inria-00000892, version 1 %% http://hal.inria.fr/inria-00000892/en/ @inproceedings{BOLDO:2005:INRIA-00000892:1, title = { {P}rovably {F}aithful {E}valuation of {P}olynomials}, author = {{B}oldo, {S}ylvie and {M}u{\~n}oz, {C}{\'e}sar}, abstract = {{W}e provide sufficient conditions that formally guarantee that the floating-point computation of a polynomial evaluation is faithful. {T}o this end, we develop a formalization of floating-point numbers and rounding modes in the {P}rogram {V}erification {S}ystem ({PVS}). {O}ur work is based on a well-known formalization of floating-point arithmetic in the proof assistant {C}oq, where polynomial evaluation has been already studied. {H}owever, thanks to the powerful proof automation provided by {PVS}, the sufficient conditions proposed in our work are more general than the original ones.}, language = {{A}nglais}, affiliation = {{PROVAL} - {INRIA} {F}uturs - {INRIA} - {U}niversit{\'e} {P}aris {S}ud - {P}aris {XI} - {N}ational {I}nstitute of {A}erospace - {NIA} - {NIA} }, booktitle = {21st {A}nnual {ACM} {S}ymposium on {A}pplied {C}omputing }, address = {{D}ijon, {F}rance }, note = {{B}.: {H}ardware/{B}.2: {ARITHMETIC} {AND} {LOGIC} {STRUCTURES}/{B}.2.3: {R}eliability, {T}esting, and {F}ault-{T}olerance, {F}.: {T}heory of {C}omputation/{F}.4: {MATHEMATICAL} {LOGIC} {AND} {FORMAL} {LANGUAGES} }, audience = {non sp{\'e}cifi{\'e}e }, month = {04}, year = {2006}, URL = {http://hal.inria.fr/inria-00000892/en/}, URL = {http://hal.inria.fr/inria-00000892/PDF/main.pdf}, }
%F inria-00000892, version 1 %0 Conference Proceedings %U http://hal.inria.fr/inria-00000892/en/ %2 INFO:INFO_LO;INFO:INFO_NA %T Provably Faithful Evaluation of Polynomials %A Boldo, Sylvie %A Muñoz, César %A Boldo, S. %A Muñoz, C. %A Boldo S. et al %+ PROVAL - INRIA Futurs - INRIA - Université Paris Sud - Paris XI - National Institute of Aerospace - NIA - NIA %X We provide sufficient conditions that formally guarantee that the floating-point computation of a polynomial evaluation is faithful. To this end, we develop a formalization of floating-point numbers and rounding modes in the Program Verification System (PVS). Our work is based on a well-known formalization of floating-point arithmetic in the proof assistant Coq, where polynomial evaluation has been already studied. However, thanks to the powerful proof automation provided by PVS, the sufficient conditions proposed in our work are more general than the original ones. %2 B.: Hardware/B.2: ARITHMETIC AND LOGIC STRUCTURES/B.2.3: Reliability, Testing, and Fault-Tolerance, F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES %G Anglais %8 2006-04 %2 non spécifiée %B 21st Annual ACM Symposium on Applied Computing %2 Dijon, France %8 2006-04
<?xml version="1.0" encoding="UTF-8"?> <listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML"> <listBibl type="inproceedings"><head>Communications avec acte</head> <biblStruct type="inproceedings" xml:id="inria-00000892"><analytic> <author><persName><forename>Sylvie</forename><surname>Boldo</surname></persName> <affiliation> <orgName type="laboratory">INRIA Futurs</orgName> <orgName type="team">PROVAL</orgName> <country>FR</country> <orgName type="institution">INRIA</orgName> <orgName type="institution">Université Paris Sud - Paris XI</orgName> </affiliation> </author> <author><persName><forename>César</forename><surname>Muñoz</surname></persName> <affiliation> <orgName type="laboratory">NIA</orgName> <orgName type="team">National Institute of Aerospace</orgName> <country>US</country> <orgName type="institution">NIA</orgName> </affiliation> </author> <title type="main" level="a">Provably Faithful Evaluation of Polynomials</title></analytic><monogr><meeting>21st Annual ACM Symposium on Applied Computing</meeting><imprint><pubPlace><settlement>Dijon</settlement><country> France</country></pubPlace><biblScope type="publicationDate">2006-04</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00000892/en/</idno><idno type="HALFile">http://hal.inria.fr/inria-00000892/PDF/main.pdf</idno></biblStruct> </listBibl> </listBibl>
Erreur :
Erreur au niveau de la base de données
Contactez-nous...
BibTeX EndNote TEI RefWorks