1: \begin{thebibliography}{10}
2:
3: \bibitem{BerCas04}
4: Y.~Bertot and P.~Casteran.
5: \newblock {\em Interactive Theorem Proving and Program Development}.
6: \newblock Springer-Verlag, 2004.
7:
8: \bibitem{BolFil07}
9: S.~Boldo and J.-C. Filliâtre.
10: \newblock Formal verification of floating point programs.
11: \newblock In {\em Proceedings of the 18th Symposium on Computer Arithmetic},
12: Montpellier, France, 2007.
13:
14: \bibitem{DauMel04}
15: M.~Daumas and G.~Melquiond.
16: \newblock Generating formally certified bounds on values and round-off errors.
17: \newblock In {\em Real Numbers and Computers}, pages 55--70, Dagstuhl, Germany,
18: 2004.
19:
20: \bibitem{DauMel07}
21: M.~Daumas and G.~Melquiond.
22: \newblock Generating certified properties for numerical expressions and their
23: evaluations.
24: \newblock Technical Report hal-00127769, Centre pour la Communication
25: Scientifique Directe, Villeurbanne, France, 2007.
26:
27: \bibitem{DauMelMun05}
28: M.~Daumas, G.~Melquiond, and C.~Mu{\~n}oz.
29: \newblock Guaranteed proofs using interval arithmetic.
30: \newblock In P.~Montuschi and E.~Schwarz, editors, {\em Proceedings of the 17th
31: Symposium on Computer Arithmetic}, pages 188--195, Cape Cod, Massachusetts,
32: 2005.
33:
34: \bibitem{DinLauMel06}
35: F.~de~Dinechin, C.~Q. Lauter, and G.~Melquiond.
36: \newblock Assisted verification of elementary functions using {G}appa.
37: \newblock In {\em Proceedings of the 2006 ACM Symposium on Applied Computing},
38: pages 1318--1322, Dijon, France, 2006.
39:
40: \bibitem{jgd:2004:issac}
41: J.-G. Dumas, P.~Giorgi, and C.~Pernet.
42: \newblock {FFPACK}: Finite field linear algebra package.
43: \newblock In {\em ISSAC '04: Proceedings of the 2004 international symposium on
44: Symbolic and algebraic computation}, pages 63--74, New York, NY, USA, 2004.
45: ACM Press.
46:
47: \bibitem{EGGSV06-1}
48: W.~Eberly, M.~Giesbrecht, P.~Giorgi, A.~Storjohann, and G.~Villard.
49: \newblock Solving sparse rational linear systems.
50: \newblock In {\em ISSAC '06: Proceedings of the 2006 international symposium on
51: Symbolic and algebraic computation}, pages 63--70, New York, NY, USA, 2006.
52: ACM Press.
53:
54: \bibitem{FilMar07}
55: J.-C. Filli\^atre and C.~March\'e.
56: \newblock The {Why/Krakatoa/Caduceus} platform for deductive program
57: verification.
58: \newblock In W.~Damm and H.~Hermanns, editors, {\em 19th International
59: Conference on Computer Aided Verification}, pages 173--177, Berlin, Germany,
60: 2007.
61:
62: \bibitem{Gol91}
63: D.~Goldberg.
64: \newblock What every computer scientist should know about floating point
65: arithmetic.
66: \newblock {\em ACM Computing Surveys}, 23(1):5--47, 1991.
67:
68: \bibitem{2002:gotoblas}
69: K.~Goto and R.~van~de Geijn.
70: \newblock On reducing {TLB} misses in matrix multiplication.
71: \newblock Technical report, University of Texas, 2002.
72: \newblock FLAME working note \#9.
73:
74: \bibitem{Har2Ka}
75: J.~Harrison.
76: \newblock Formal verification of floating point trigonometric functions.
77: \newblock In W.~A. Hunt and S.~D. Johnson, editors, {\em Proceedings of the
78: Third International Conference on Formal Methods in Computer-Aided Design},
79: pages 217--233, Austin, Texas, 2000.
80:
81: \bibitem{JauKieDidWal01}
82: L.~Jaulin, M.~Kieffer, O.~Didrit, and E.~Walter.
83: \newblock {\em Applied interval analysis}.
84: \newblock Springer, 2001.
85:
86: \bibitem{MelPio07}
87: G.~Melquiond and S.~Pion.
88: \newblock Formally certified floating-point filters for homogeneous geometric
89: predicates.
90: \newblock {\em Theoretical Informatics and Applications}, 2007.
91: \newblock To appear.
92:
93: \bibitem{MicTisVey06}
94: R.~Michard, A.~Tisserand, and N.~Veyrat-Charvillon.
95: \newblock Optimisation d'opérateurs arithmétiques matériels à base
96: d'approximations polynomiales.
97: \newblock In {\em Symposium en Architecture de Machines}, pages 1318--1322,
98: Perpignan, France, 2006.
99:
100: \bibitem{RusHen91}
101: J.~Rushby and F.~von Henke.
102: \newblock Formal verification of algorithms for critical systems.
103: \newblock In {\em Proceedings of the Conference on Software for Critical
104: Systems}, pages 1--15, New Orleans, Louisiana, 1991.
105:
106: \bibitem{TiwShaRus03}
107: A.~Tiwari, N.~Shankar, and J.~Rushby.
108: \newblock Invisible formal methods for embedded control systems.
109: \newblock {\em Proceedings of the IEEE}, 91(1):29--39, 2003.
110:
111: \bibitem{Whaley:2001:AEO}
112: R.~C. Whaley, A.~Petitet, and J.~J. Dongarra.
113: \newblock Automated empirical optimizations of software and the {ATLAS}
114: project.
115: \newblock {\em Parallel Computing}, 27(1--2):3--35, Jan. 2001.
116: \newblock
117: \texttt{www.elsevier.nl/gej-ng/10/\-35/\-21/\-47/\-25/\-23/article.pdf}.
118:
119: \end{thebibliography}
120: