1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\citeauthoryear{Boldo and Daumas}{Boldo and
4: Daumas}{2004}]{BolDau04b}
5: {\sc Boldo, S.} {\sc and} {\sc Daumas, M.} 2004.
6: \newblock A simple test qualifying the accuracy of {H}orner's rule for
7: polynomials.
8: \newblock {\em Numerical Algorithms\/}~{\em 37,\/}~1-4, 45--60.
9:
10: \bibitem[\protect\citeauthoryear{Boldo and Filliâtre}{Boldo and
11: Filliâtre}{2007}]{BolFil07}
12: {\sc Boldo, S.} {\sc and} {\sc Filliâtre, J.-C.} 2007.
13: \newblock Formal verification of floating point programs.
14: \newblock In {\em Proceedings of the 18th Symposium on Computer Arithmetic}.
15: Montpellier, France.
16:
17: \bibitem[\protect\citeauthoryear{Boldo and Melquiond}{Boldo and
18: Melquiond}{2005}]{BolMel05}
19: {\sc Boldo, S.} {\sc and} {\sc Melquiond, G.} 2005.
20: \newblock When double rounding is odd.
21: \newblock In {\em Proceedings of the 15th IMACS World Congress on Computational
22: and Applied Mathematics}. Paris, France.
23:
24: \bibitem[\protect\citeauthoryear{Boutin}{Boutin}{1997}]{Bou97}
25: {\sc Boutin, S.} 1997.
26: \newblock Using reflection to build efficient and certified decision
27: procedures.
28: \newblock In {\em Proceedings of the Third International Symposium on
29: Theoretical Aspects of Computer Software}. London, United Kingdom, 515--529.
30:
31: \bibitem[\protect\citeauthoryear{Brönnimann, Melquiond, and Pion}{Brönnimann
32: et~al\mbox{.}}{2003}]{BroMelPio03}
33: {\sc Brönnimann, H.}, {\sc Melquiond, G.}, {\sc and} {\sc Pion, S.} 2003.
34: \newblock The {B}oost interval arithmetic library.
35: \newblock In {\em Real Numbers and Computers}. Lyon, France, 65--80.
36:
37: \bibitem[\protect\citeauthoryear{Daumas and Giorgi}{Daumas and
38: Giorgi}{2007}]{DauGio07}
39: {\sc Daumas, M.} {\sc and} {\sc Giorgi, P.} 2007.
40: \newblock Proof checking for delayed finite field arithmetic using floating
41: point operators.
42: \newblock Tech. Rep. hal-00135090, Centre pour la Communication Scientifique
43: Directe, Villeurbanne, France.
44:
45: \bibitem[\protect\citeauthoryear{Daumas and Melquiond}{Daumas and
46: Melquiond}{2004}]{DauMel04}
47: {\sc Daumas, M.} {\sc and} {\sc Melquiond, G.} 2004.
48: \newblock Generating formally certified bounds on values and round-off errors.
49: \newblock In {\em Real Numbers and Computers}. Dagstuhl, Germany, 55--70.
50:
51: \bibitem[\protect\citeauthoryear{Daumas, Melquiond, and Mu{\~n}oz}{Daumas
52: et~al\mbox{.}}{2005}]{DauMelMun05}
53: {\sc Daumas, M.}, {\sc Melquiond, G.}, {\sc and} {\sc Mu{\~n}oz, C.} 2005.
54: \newblock Guaranteed proofs using interval arithmetic.
55: \newblock In {\em Proceedings of the 17th Symposium on Computer Arithmetic},
56: {P.~Montuschi} {and} {E.~Schwarz}, Eds. Cape Cod, Massachusetts, 188--195.
57:
58: \bibitem[\protect\citeauthoryear{de~Dinechin, Defour, and Lauter}{de~Dinechin
59: et~al\mbox{.}}{2004}]{DinDefLau04}
60: {\sc de~Dinechin, F.}, {\sc Defour, D.}, {\sc and} {\sc Lauter, C.} 2004.
61: \newblock Fast correct rounding of elementary functions in double precision
62: using double-extended arithmetic.
63: \newblock Research report 5137, Institut National de Recherche en Informatique
64: et en Automatique, Le Chesnay, France.
65:
66: \bibitem[\protect\citeauthoryear{de~Dinechin, Lauter, and
67: Melquiond}{de~Dinechin et~al\mbox{.}}{2006}]{DinLauMel06}
68: {\sc de~Dinechin, F.}, {\sc Lauter, C.~Q.}, {\sc and} {\sc Melquiond, G.} 2006.
69: \newblock Assisted verification of elementary functions using {G}appa.
70: \newblock In {\em Proceedings of the 2006 ACM Symposium on Applied Computing}.
71: Dijon, France, 1318--1322.
72:
73: \bibitem[\protect\citeauthoryear{Even and Seidel}{Even and
74: Seidel}{1999}]{EveSei99}
75: {\sc Even, G.} {\sc and} {\sc Seidel, P.-M.} 1999.
76: \newblock A comparison of three rounding algorithms for {IEEE} floating-point
77: multiplication.
78: \newblock In {\em Proceedings of the 14th Symposium on Computer Arithmetic},
79: {I.~Koren} {and} {P.~Kornerup}, Eds. Adelaide, Australia, 225--232.
80:
81: \bibitem[\protect\citeauthoryear{Filli\^atre}{Filli\^atre}{2003}]{Fil03}
82: {\sc Filli\^atre, J.-C.} 2003.
83: \newblock Why: a multi-language multi-prover verification tool.
84: \newblock Research Report 1366, Universit\'e Paris Sud.
85:
86: \bibitem[\protect\citeauthoryear{Fousse, Hanrot, Lef{\`e}vre, P{\'e}lissier,
87: and Zimmermann}{Fousse et~al\mbox{.}}{2005}]{FouHanLefPelZim05}
88: {\sc Fousse, L.}, {\sc Hanrot, G.}, {\sc Lef{\`e}vre, V.}, {\sc P{\'e}lissier,
89: P.}, {\sc and} {\sc Zimmermann, P.} 2005.
90: \newblock {MPFR}: A multiple-precision binary floating-point library with
91: correct rounding.
92: \newblock Tech. Rep. RR-5753, {INRIA}.
93:
94: \bibitem[\protect\citeauthoryear{Gameiro and Manolios}{Gameiro and
95: Manolios}{2004}]{GamMan04}
96: {\sc Gameiro, M.} {\sc and} {\sc Manolios, P.} 2004.
97: \newblock Formally verifying an algorithm based on interval arithmetic for
98: checking transversality.
99: \newblock In {\em Fifth International Workshop on the ACL2 Theorem Prover and
100: Its Applications}. Austin, Texas, 17.
101:
102: \bibitem[\protect\citeauthoryear{Harrison}{Harrison}{1997}]{Har97a}
103: {\sc Harrison, J.} 1997.
104: \newblock Floating point verification in {HOL} light: the exponential function.
105: \newblock Technical Report 428, University of Cambridge Computer Laboratory.
106:
107: \bibitem[\protect\citeauthoryear{Harrison}{Harrison}{2000}]{Har2Kb}
108: {\sc Harrison, J.} 2000.
109: \newblock {\em The {HOL} {L}ight manual}.
110: \newblock Version 1.1.
111:
112: \bibitem[\protect\citeauthoryear{Higham}{Higham}{2002}]{Hig02}
113: {\sc Higham, N.~J.} 2002.
114: \newblock {\em Accuracy and stability of numerical algorithms}.
115: \newblock SIAM.
116: \newblock Second edition.
117:
118: \bibitem[\protect\citeauthoryear{Huet, Kahn, and Paulin-Mohring}{Huet
119: et~al\mbox{.}}{2004}]{HueKahPau04}
120: {\sc Huet, G.}, {\sc Kahn, G.}, {\sc and} {\sc Paulin-Mohring, C.} 2004.
121: \newblock {\em The {Coq} proof assistant: a tutorial: version 8.0}.
122:
123: \bibitem[\protect\citeauthoryear{Jaulin, Kieffer, Didrit, and Walter}{Jaulin
124: et~al\mbox{.}}{2001}]{JauKieDidWal01}
125: {\sc Jaulin, L.}, {\sc Kieffer, M.}, {\sc Didrit, O.}, {\sc and} {\sc Walter,
126: E.} 2001.
127: \newblock {\em Applied interval analysis}.
128: \newblock Springer.
129:
130: \bibitem[\protect\citeauthoryear{Kahan}{Kahan}{1965}]{Kah65}
131: {\sc Kahan, W.} 1965.
132: \newblock Further remarks on reducing truncation errors.
133: \newblock {\em Communications of the ACM\/}~{\em 8,\/}~1, 40.
134:
135: \bibitem[\protect\citeauthoryear{Kaufmann, Manolios, and Moore}{Kaufmann
136: et~al\mbox{.}}{2000}]{KauManMoo2K}
137: {\sc Kaufmann, M.}, {\sc Manolios, P.}, {\sc and} {\sc Moore, J.~S.} 2000.
138: \newblock {\em Computer-Aided Reasoning: An Approach}.
139: \newblock Kluwer Academic Publishers.
140:
141: \bibitem[\protect\citeauthoryear{Melquiond and Pion}{Melquiond and
142: Pion}{2007}]{MelPio07}
143: {\sc Melquiond, G.} {\sc and} {\sc Pion, S.} 2007.
144: \newblock Formally certified floating-point filters for homogeneous geometric
145: predicates.
146: \newblock {\em Theoretical Informatics and Applications\/}.
147: \newblock To appear.
148:
149: \bibitem[\protect\citeauthoryear{Michard, Tisserand, and
150: Veyrat-Charvillon}{Michard et~al\mbox{.}}{2006}]{MicTisVey06}
151: {\sc Michard, R.}, {\sc Tisserand, A.}, {\sc and} {\sc Veyrat-Charvillon, N.}
152: 2006.
153: \newblock Optimisation d'opérateurs arithmétiques matériels ŕ base
154: d'approximations polynomiales.
155: \newblock In {\em Symposium en Architecture de Machines}. Perpignan, France,
156: 1318--1322.
157:
158: \bibitem[\protect\citeauthoryear{Neumaier}{Neumaier}{1990}]{Neu90}
159: {\sc Neumaier, A.} 1990.
160: \newblock {\em Interval methods for systems of equations}.
161: \newblock Cambridge University Press.
162:
163: \bibitem[\protect\citeauthoryear{Owre, Rushby, and Shankar}{Owre
164: et~al\mbox{.}}{1992}]{OwrRusSha92}
165: {\sc Owre, S.}, {\sc Rushby, J.~M.}, {\sc and} {\sc Shankar, N.} 1992.
166: \newblock {PVS}: a prototype verification system.
167: \newblock In {\em 11th International Conference on Automated Deduction},
168: {D.~Kapur}, Ed. Springer-Verlag, Saratoga, New-York, 748--752.
169:
170: \bibitem[\protect\citeauthoryear{Putot, Goubault, and Martel}{Putot
171: et~al\mbox{.}}{2004}]{PutGouMar04}
172: {\sc Putot, S.}, {\sc Goubault, E.}, {\sc and} {\sc Martel, M.} 2004.
173: \newblock Static analysis based validation of floating point computations.
174: \newblock In {\em Novel Approaches to Verification}. Lecture Notes in Computer
175: Science, vol. 2991. Dagstuhl, Germany, 306--313.
176:
177: \bibitem[\protect\citeauthoryear{Revy}{Revy}{2006}]{Rev06}
178: {\sc Revy, G.} 2006.
179: \newblock Analyse et implantation d'algorithmes rapides pour l'{\'e}valuation
180: polynomiale sur les nombres flottants.
181: \newblock Tech. Rep. ensl-00119498, École Normale Supérieure de Lyon.
182:
183: \bibitem[\protect\citeauthoryear{{Rockwell Collins}}{{Rockwell
184: Collins}}{2005}]{Roc05}
185: {\sc {Rockwell Collins}}. 2005.
186: \newblock {R}ockwell {C}ollins receives {MILS} certification from {NSA} on
187: microprocessor.
188: \newblock Press Releases.
189:
190: \bibitem[\protect\citeauthoryear{Rump, Ogita, and Oishi}{Rump
191: et~al\mbox{.}}{2005}]{RumOgiOis05}
192: {\sc Rump, S.~M.}, {\sc Ogita, T.}, {\sc and} {\sc Oishi, S.} 2005.
193: \newblock Accurate floating-point summation.
194: \newblock Tech. Rep. 05.12, Hamburg University of Technology, Hamburg, Germany.
195:
196: \bibitem[\protect\citeauthoryear{{Schlumberger}}{{Schlumberger}}{2003}]{Sch03}
197: {\sc {Schlumberger}}. 2003.
198: \newblock {S}chlumberger leads the way in smart card security with common
199: criteria {EAL}7 security methodology.
200: \newblock Press Releases.
201:
202: \bibitem[\protect\citeauthoryear{Stevenson et~al\mbox{.}}{Stevenson
203: et~al\mbox{.}}{1987}]{Ste.87}
204: {\sc Stevenson, D.} {\sc et~al\mbox{.}} 1987.
205: \newblock An {A}merican national standard: {IEEE} standard for binary floating
206: point arithmetic.
207: \newblock {\em ACM SIGPLAN Notices\/}~{\em 22,\/}~2, 9--25.
208:
209: \bibitem[\protect\citeauthoryear{Tang}{Tang}{1989}]{Tan89}
210: {\sc Tang, P. T.~P.} 1989.
211: \newblock Table driven implementation of the exponential function in {IEEE}
212: floating point arithmetic.
213: \newblock {\em ACM Transactions on Mathematical Software\/}~{\em 15,\/}~2,
214: 144--157.
215:
216: \bibitem[\protect\citeauthoryear{Texas Instruments}{Texas
217: Instruments}{1997}]{Tex97}
218: Texas Instruments 1997.
219: \newblock {\em {TMS320C3x} --- User's guide}.
220: \newblock Texas Instruments.
221:
222: \bibitem[\protect\citeauthoryear{Tiwari, Shankar, and Rushby}{Tiwari
223: et~al\mbox{.}}{2003}]{TiwShaRus03}
224: {\sc Tiwari, A.}, {\sc Shankar, N.}, {\sc and} {\sc Rushby, J.} 2003.
225: \newblock Invisible formal methods for embedded control systems.
226: \newblock {\em Proceedings of the IEEE\/}~{\em 91,\/}~1, 29--39.
227:
228: \end{thebibliography}
229: