1: \begin{thebibliography}{10}
2: \providecommand{\url}[1]{#1}
3: \csname url@rmstyle\endcsname
4: \providecommand{\newblock}{\relax}
5: \providecommand{\bibinfo}[2]{#2}
6: \providecommand\BIBentrySTDinterwordspacing{\spaceskip=0pt\relax}
7: \providecommand\BIBentryALTinterwordstretchfactor{4}
8: \providecommand\BIBentryALTinterwordspacing{\spaceskip=\fontdimen2\font plus
9: \BIBentryALTinterwordstretchfactor\fontdimen3\font minus
10: \fontdimen4\font\relax}
11: \providecommand\BIBforeignlanguage[2]{{%
12: \expandafter\ifx\csname l@#1\endcsname\relax
13: \typeout{** WARNING: IEEEtran.bst: No hyphenation pattern has been}%
14: \typeout{** loaded for the language `#1'. Using the pattern for}%
15: \typeout{** the default language instead.}%
16: \else
17: \language=\csname l@#1\endcsname
18: \fi
19: #2}}
20:
21: \bibitem{JohBut92}
22: \BIBentryALTinterwordspacing
23: S.~C. Johnson and R.~W. Butler, ``Design for validation,'' \emph{IEEE Aerospace
24: and Electronic Systems Magazine}, vol.~7, no.~1, pp. 38--43, 1992. [Online].
25: Available: \url{http://dx.doi.org/10.1109/62.127129}
26: \BIBentrySTDinterwordspacing
27:
28: \bibitem{Rus98}
29: \BIBentryALTinterwordspacing
30: D.~M. Russinoff, ``A mechanically checked proof of {IEEE} compliance of the
31: floating point multiplication, division and square root algorithms of the
32: {AMD-K7} processor,'' \emph{LMS Journal of Computation and Mathematics},
33: vol.~1, pp. 148--200, 1998. [Online]. Available:
34: \url{http://www.onr.com/user/russ/david/k7-div-sqrt.ps}
35: \BIBentrySTDinterwordspacing
36:
37: \bibitem{Har2Ka}
38: \BIBentryALTinterwordspacing
39: J.~Harrison, ``Formal verification of floating point trigonometric functions,''
40: in \emph{Proceedings of the Third International Conference on Formal Methods
41: in Computer-Aided Design}, W.~A. Hunt and S.~D. Johnson, Eds., Austin, Texas,
42: 2000, pp. 217--233. [Online]. Available:
43: \url{http://www.springerlink.com/link.asp?id=wxvaqu9wjrgc8l99}
44: \BIBentrySTDinterwordspacing
45:
46: \bibitem{BolDau03}
47: \BIBentryALTinterwordspacing
48: S.~Boldo and M.~Daumas, ``Representable correcting terms for possibly
49: underflowing floating point operations,'' in \emph{Proceedings of the 16th
50: Symposium on Computer Arithmetic}, J.-C. Bajard and M.~Schulte, Eds.,
51: Santiago de Compostela, Spain, 2003, pp. 79--86. [Online]. Available:
52: \url{http://perso.ens-lyon.fr/marc.daumas/SoftArith/BolDau03.pdf}
53: \BIBentrySTDinterwordspacing
54:
55: \bibitem{DauMelMun05}
56: \BIBentryALTinterwordspacing
57: M.~Daumas, G.~Melquiond, and C.~Mu{\~n}oz, ``Guaranteed proofs using interval
58: arithmetic,'' in \emph{Proceedings of the 17th Symposium on Computer
59: Arithmetic}, P.~Montuschi and E.~Schwarz, Eds., Cape Cod, Massachusetts,
60: 2005, pp. 188--195. [Online]. Available:
61: \url{http://perso.ens-lyon.fr/marc.daumas/SoftArith/DauMelMun05.pdf}
62: \BIBentrySTDinterwordspacing
63:
64: \bibitem{MunLes05}
65: \BIBentryALTinterwordspacing
66: C.~Mu{\~n}oz and D.~Lester, ``Real number calculations and theorem proving,''
67: in \emph{18th International Conference on Theorem Proving in Higher Order
68: Logics}, Oxford, England, 2005, pp. 239--254. [Online]. Available:
69: \url{http://dx.doi.org/10.1007/11541868_13}
70: \BIBentrySTDinterwordspacing
71:
72: \bibitem{GorMel93}
73: M.~J.~C. Gordon and T.~F. Melham, Eds., \emph{Introduction to {HOL}: {A}
74: theorem proving environment for higher order logic}.\hskip 1em plus 0.5em
75: minus 0.4em\relax Cambridge University Press, 1993.
76:
77: \bibitem{HueKahPau04}
78: \BIBentryALTinterwordspacing
79: G.~Huet, G.~Kahn, and C.~Paulin-Mohring, \emph{The {Coq} proof assistant: a
80: tutorial: version 8.0}, 2004. [Online]. Available:
81: \url{ftp://ftp.inria.fr/INRIA/coq/current/doc/Tutorial.pdf.gz}
82: \BIBentrySTDinterwordspacing
83:
84: \bibitem{OwrRusSha92}
85: \BIBentryALTinterwordspacing
86: S.~Owre, J.~M. Rushby, and N.~Shankar, ``{PVS}: a prototype verification
87: system,'' in \emph{11th International Conference on Automated Deduction},
88: D.~Kapur, Ed.\hskip 1em plus 0.5em minus 0.4em\relax Saratoga, New-York:
89: Springer-Verlag, 1992, pp. 748--752. [Online]. Available:
90: \url{http://pvs.csl.sri.com/papers/cade92-pvs/cade92-pvs.ps}
91: \BIBentrySTDinterwordspacing
92:
93: \bibitem{Bre98}
94: P.~Br\'emaud, \emph{Markov chains: {G}ibbs fields, {M}onte {C}arlo simulation,
95: and queues}.\hskip 1em plus 0.5em minus 0.4em\relax Springer, 1998.
96:
97: \bibitem{Fuh04}
98: \BIBentryALTinterwordspacing
99: C.-D. Fuh, ``Uniform {M}arkov renewal theory and ruin probabilities in {M}arkov
100: random walks,'' \emph{Annals of Applied Probability}, vol.~14, no.~3, pp.
101: 1202--1241, 2004. [Online]. Available:
102: \url{http://dx.doi.org/10.1214/105051604000000260}
103: \BIBentrySTDinterwordspacing
104:
105: \bibitem{Asm2K}
106: S.~Asmussen, \emph{Ruin Probabilities}.\hskip 1em plus 0.5em minus 0.4em\relax
107: World Scientific, 2000.
108:
109: \bibitem{GriSti82}
110: G.~R. Grimmett and D.~R. Stirzaker, \emph{Probability and Random
111: Processes}.\hskip 1em plus 0.5em minus 0.4em\relax Oxford University Press,
112: 1982.
113:
114: \bibitem{Hur02}
115: \BIBentryALTinterwordspacing
116: J.~Hurd, ``Formal verification of probabilistic algorithms,'' Ph.D.
117: dissertation, University of Cambridge, 2002. [Online]. Available:
118: \url{http://www.cl.cam.ac.uk/~jeh1004/research/papers/thesis.pdf}
119: \BIBentrySTDinterwordspacing
120:
121: \bibitem{AudPau06}
122: \BIBentryALTinterwordspacing
123: P.~Audebaud and C.~Paulin-Mohring, ``Proofs of randomized algorithms in
124: {C}oq,'' in \emph{Proceedings of the 8th International Conference on
125: Mathematics of Program Construction}, T.~Uustalu, Ed., Kuressaare, Estonia,
126: 2006, pp. 49--68. [Online]. Available:
127: \url{http://dx.doi.org/10.1007/11783596_6}
128: \BIBentrySTDinterwordspacing
129:
130: \bibitem{Gol91}
131: \BIBentryALTinterwordspacing
132: D.~Goldberg, ``What every computer scientist should know about floating point
133: arithmetic,'' \emph{ACM Computing Surveys}, vol.~23, no.~1, pp. 5--47, 1991.
134: [Online]. Available: \url{http://doi.acm.org/10.1145/103162.103163}
135: \BIBentrySTDinterwordspacing
136:
137: \bibitem{Ste.87}
138: D.~Stevenson \emph{et~al.}, ``An {A}merican national standard: {IEEE} standard
139: for binary floating point arithmetic,'' \emph{ACM SIGPLAN Notices}, vol.~22,
140: no.~2, pp. 9--25, 1987.
141:
142: \bibitem{Tex97}
143: \BIBentryALTinterwordspacing
144: \emph{{TMS320C3x} --- User's guide}, Texas Instruments, 1997. [Online].
145: Available: \url{http://www-s.ti.com/sc/psheets/spru031e/spru031e.pdf}
146: \BIBentrySTDinterwordspacing
147:
148: \bibitem{Knu97}
149: D.~E. Knuth, \emph{The Art of Computer Programming: Seminumerical
150: Algorithms}.\hskip 1em plus 0.5em minus 0.4em\relax Addison-Wesley, 1997,
151: third edition.
152:
153: \bibitem{FelGoo76}
154: \BIBentryALTinterwordspacing
155: A.~Feldstein and R.~Goodman, ``Convergence estimates for the distribution of
156: trailing digits,'' \emph{Journal of the ACM}, vol.~23, no.~2, pp. 287--297,
157: 1976. [Online]. Available: \url{http://doi.acm.org/10.1145/321941.321948}
158: \BIBentrySTDinterwordspacing
159:
160: \bibitem{BusFelGooLin79}
161: \BIBentryALTinterwordspacing
162: J.~Bustoz, A.~Feldstein, R.~Goodman, and S.~Linnainmaa, ``Improved trailing
163: digits estimates applied to optimal computer arithmetic,'' \emph{Journal of
164: the ACM}, vol.~26, no.~4, pp. 716 -- 730, 1979. [Online]. Available:
165: \url{http://doi.acm.org/10.1145/322154.322162}
166: \BIBentrySTDinterwordspacing
167:
168: \bibitem{BriDauLanMar06}
169: N.~Brisebarre, M.~Daumas, P.~Langlois, and M.~Martel, ``Survol et limitations
170: des modèles discrets-continus pour la sûreté numérique,'' Centre pour la
171: Communication Scientifique et Directe, Villeurbanne, France, Tech. Rep.,
172: 2006.
173:
174: \bibitem{StoBur02}
175: \BIBentryALTinterwordspacing
176: J.~Stoer and R.~Bulirsch, \emph{Introduction to Numerical Analysis}.\hskip 1em
177: plus 0.5em minus 0.4em\relax Springer Verlag, 2002. [Online]. Available:
178: \url{http://www.springer.de/cgi/svcat/search_book.pl?isbn=0-387-95452-X}
179: \BIBentrySTDinterwordspacing
180:
181: \bibitem{JauKieDidWal01}
182: \BIBentryALTinterwordspacing
183: L.~Jaulin, M.~Kieffer, O.~Didrit, and E.~Walter, \emph{Applied interval
184: analysis}.\hskip 1em plus 0.5em minus 0.4em\relax Springer, 2001. [Online].
185: Available:
186: \url{http://www.springeronline.com/sgw/cda/frontpage/0,10735,5-40106-22-2093%
187: 571-0,00.html}
188: \BIBentrySTDinterwordspacing
189:
190: \bibitem{GouMarPut06}
191: \BIBentryALTinterwordspacing
192: E.~Goubault, M.~Martel, and S.~Putot, ``Some future challenges in the
193: validation of control systems,'' in \emph{European Congress on Embedded Real
194: Time Software}, Toulouse, France, 2006. [Online]. Available:
195: \url{http://www.enseignement.polytechnique.fr/profs/informatique/Matthieu.Ma%
196: rtel/erts.pdf}
197: \BIBentrySTDinterwordspacing
198:
199: \bibitem{Hal44}
200: P.~R. Halmos, ``The foundations of probability,'' \emph{American Mathematical
201: Monthly}, vol.~51, pp. 493--510, 1944.
202:
203: \bibitem{Hal50}
204: ------, \emph{Measure Theory}.\hskip 1em plus 0.5em minus 0.4em\relax Van
205: Nostrand Reinhold, 1950.
206:
207: \end{thebibliography}
208: