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{USA.92}
22: \BIBentryALTinterwordspacing
23: {Information Management and Technology Division}, ``Patriot missile defense:
24: software problem led to system failure at {D}hahran, {S}audi {A}rabia,''
25: United States General Accounting Office, Report B-247094, 1992. [Online].
26: Available: \url{http://www.fas.org/spp/starwars/gao/im92026.htm}
27: \BIBentrySTDinterwordspacing
28:
29: \bibitem{Lio.96}
30: \BIBentryALTinterwordspacing
31: J.-L. Lions \emph{et~al.}, ``Ariane 5 flight 501 failure report by the inquiry
32: board,'' European Space Agency, Paris, France, Tech. Rep., 1996. [Online].
33: Available: \url{http://ravel.esrin.esa.it/docs/esa-x-1819eng.pdf}
34: \BIBentrySTDinterwordspacing
35:
36: \bibitem{GagMcC04}
37: \BIBentryALTinterwordspacing
38: D.~Gage and J.~McCormick, ``We did nothing wrong,'' \emph{Baseline}, vol.~1,
39: no.~28, pp. 32--58, 2004. [Online]. Available:
40: \url{http://common.ziffdavisinternet.com/download/0/2529/Baseline0304-Dissec%
41: tionNEW.pdf}
42: \BIBentrySTDinterwordspacing
43:
44: \bibitem{Har98}
45: J.~Harrison, \emph{Theorem Proving with the Real Numbers}.\hskip 1em plus 0.5em
46: minus 0.4em\relax Springer-Verlag, 1998.
47:
48: \bibitem{FlePau2K}
49: \BIBentryALTinterwordspacing
50: J.~Fleuriot and L.~Paulson, ``Mechanizing nonstandard real analysis,''
51: \emph{LMS Journal of Computation and Mathematics}, vol.~3, pp. 140--190,
52: 2000. [Online]. Available: \url{http://www.lms.ac.uk/jcm/3/lms1999-027/}
53: \BIBentrySTDinterwordspacing
54:
55: \bibitem{Gam99}
56: \BIBentryALTinterwordspacing
57: R.~Gamboa, ``Mechanically verifying real-valued algorithms in {ACL2},'' Ph.D.
58: dissertation, University of Texas at Austin, 1999. [Online]. Available:
59: \url{ftp://ftp.cs.utexas.edu/pub/boyer/diss/gamboa.pdf}
60: \BIBentrySTDinterwordspacing
61:
62: \bibitem{May01}
63: \BIBentryALTinterwordspacing
64: M.~Mayero, ``Formalisation et automatisation de preuves en analyse r{\'e}elle
65: et num{\'e}rique,'' Ph.D. dissertation, Universit{\'e} Pierre et Marie Curie,
66: Paris, France, 2001. [Online]. Available:
67: \url{http://www.pps.jussieu.fr/~mayero/specif/these-mayero.ps}
68: \BIBentrySTDinterwordspacing
69:
70: \bibitem{Got02}
71: \BIBentryALTinterwordspacing
72: H.~Gottliebsen, ``Automated theorem proving for mathematics: real analysis in
73: {PVS},'' Ph.D. dissertation, University of St Andrews, 2001. [Online].
74: Available: \url{http://www.dcs.qmul.ac.uk/~hago/thesis.ps.gz}
75: \BIBentrySTDinterwordspacing
76:
77: \bibitem{MunCarDowBut03}
78: \BIBentryALTinterwordspacing
79: C.~Mu{\~n}oz, V.~Carre{\~n}o, G.~Dowek, and R.~Butler, ``Formal verification of
80: conflict detection algorithms,'' \emph{International Journal on Software
81: Tools for Technology Transfer}, vol.~4, no.~3, pp. 371--380, 2003. [Online].
82: Available: \url{http://dx.doi.org/10.1007/s10009-002-0084-3}
83: \BIBentrySTDinterwordspacing
84:
85: \bibitem{DauMelMun05}
86: \BIBentryALTinterwordspacing
87: M.~Daumas, G.~Melquiond, and C.~Mu{\~n}oz, ``Guaranteed proofs using interval
88: arithmetic,'' in \emph{Proceedings of the 17th Symposium on Computer
89: Arithmetic}, P.~Montuschi and E.~Schwarz, Eds., Cape Cod, Massachusetts,
90: 2005, pp. 188--195. [Online]. Available:
91: \url{http://hal.archives-ouvertes.fr/hal-00164621}
92: \BIBentrySTDinterwordspacing
93:
94: \bibitem{MunLes05}
95: \BIBentryALTinterwordspacing
96: C.~Mu{\~n}oz and D.~Lester, ``Real number calculations and theorem proving,''
97: in \emph{18th International Conference on Theorem Proving in Higher Order
98: Logics}, Oxford, England, 2005, pp. 239--254. [Online]. Available:
99: \url{http://dx.doi.org/10.1007/11541868_13}
100: \BIBentrySTDinterwordspacing
101:
102: \bibitem{OwrRusSha92}
103: \BIBentryALTinterwordspacing
104: S.~Owre, J.~M. Rushby, and N.~Shankar, ``{PVS}: a prototype verification
105: system,'' in \emph{11th International Conference on Automated Deduction},
106: D.~Kapur, Ed.\hskip 1em plus 0.5em minus 0.4em\relax Saratoga, New-York:
107: Springer-Verlag, 1992, pp. 748--752. [Online]. Available:
108: \url{http://pvs.csl.sri.com/papers/cade92-pvs/cade92-pvs.ps}
109: \BIBentrySTDinterwordspacing
110:
111: \bibitem{AbrSte72}
112: M.~Abramowitz and I.~A. Stegun, Eds., \emph{Handbook of mathematical functions
113: with formulas, graphs, and mathematical tables}.\hskip 1em plus 0.5em minus
114: 0.4em\relax Dover publications, 1972, ninth printing.
115:
116: \bibitem{Mul06}
117: \BIBentryALTinterwordspacing
118: J.-M. Muller, \emph{Elementary functions, algorithms and implementation}.\hskip
119: 1em plus 0.5em minus 0.4em\relax Birkhauser, 2006. [Online]. Available:
120: \url{http://www.springer.com/west/home/birkhauser/computer+science?SGWID=4-4%
121: 0353-22-72377986-0}
122: \BIBentrySTDinterwordspacing
123:
124: \bibitem{Neu90}
125: A.~Neumaier, \emph{Interval methods for systems of equations}.\hskip 1em plus
126: 0.5em minus 0.4em\relax Cambridge University Press, 1990.
127:
128: \bibitem{JauKieDidWal01}
129: \BIBentryALTinterwordspacing
130: L.~Jaulin, M.~Kieffer, O.~Didrit, and E.~Walter, \emph{Applied interval
131: analysis}.\hskip 1em plus 0.5em minus 0.4em\relax Springer, 2001. [Online].
132: Available:
133: \url{http://www.springeronline.com/sgw/cda/frontpage/0,10735,5-40106-22-2093%
134: 571-0,00.html}
135: \BIBentrySTDinterwordspacing
136:
137: \bibitem{Kea96}
138: R.~B. Kearfott, Ed., \emph{Rigorous global search: continuous problemes}.\hskip
139: 1em plus 0.5em minus 0.4em\relax Kluwer Academic Publishers, 1996.
140:
141: \bibitem{Yak92}
142: A.~Yakovlev, ``Classification approach to programming of localizational
143: (interval) computations,'' \emph{Interval Computations}, vol.~1, no.~1, pp.
144: 61--84, 1992.
145:
146: \bibitem{Saw02}
147: J.~Sawada, ``Formal verification of divide and square root algorithms using
148: series calculation,'' in \emph{3rd International Workshop on the ACL2 Theorem
149: Prover and its Applications}.\hskip 1em plus 0.5em minus 0.4em\relax
150: University of Grenoble, 2002, pp. 31--49.
151:
152: \bibitem{Mun07NIA}
153: C.~Mu{\~{n}}oz, ``Batch proving and proof scripting in {PVS},'' NIA-NASA
154: Langley, National Institute of Aerospace, Hampton, VA, Report NIA Report No.
155: 2007-03, NASA/CR-2007-214546, February 2007.
156:
157: \bibitem{Mar2K}
158: P.~Markstein, \emph{{IA}-64 and elementary functions: speed and
159: precision}.\hskip 1em plus 0.5em minus 0.4em\relax Prentice Hall, 2000.
160:
161: \bibitem{har95}
162: J.~Harrison, ``Metatheory and reflection in theorem proving: A survey and
163: critique,'' SRI Cambridge, Millers Yard, Cambridge, UK, Technical Report
164: CRC-053, 1995.
165:
166: \bibitem{Bou97}
167: S.~Boutin, ``Using reflection to build efficient and certified decision
168: procedures,'' in \emph{Proceedings of the Third International Symposium on
169: Theoretical Aspects of Computer Software}, London, United Kingdom, 1997, pp.
170: 515--529.
171:
172: \bibitem{vHPP98}
173: F.~W. von Henke, S.~Pfab, H.~Pfeifer, and H.~Rue{\ss}, ``{Case Studies in
174: Meta-Level Theorem Proving},'' in \emph{Proc. Intl. Conf. on Theorem Proving
175: in Higher Order Logics}, ser. Lecture Notes in Computer Science, J.~Grundy
176: and M.~Newey, Eds., no. 1479.\hskip 1em plus 0.5em minus 0.4em\relax
177: Springer-Verlag, Sept. 1998, pp. 461--478.
178:
179: \bibitem{Sha99}
180: N.~Shankar, ``Efficiently executing {PVS},'' Computer Science Laboratory, SRI
181: International, Menlo Park, CA, Project report, Nov. 1999, available at
182: \url{http://www.csl.sri.com/shankar/PVSeval.ps.gz}.
183:
184: \bibitem{Mun03NIA}
185: C.~Mu{\~{n}}oz, ``Rapid prototyping in {PVS},'' NIA-NASA Langley, National
186: Institute of Aerospace, Hampton, VA, Report NIA Report No. 2003-03,
187: NASA/CR-2003-212418, May 2003.
188:
189: \bibitem{GowLes2K}
190: \BIBentryALTinterwordspacing
191: P.~Gowland and D.~Lester, ``A survey of exact arithmetic implementations,'' in
192: \emph{4th International Workshop on Computability and Complexity in
193: Analysis}, Swansea, United Kingdom, 2000, pp. 30--47. [Online]. Available:
194: \url{http://www.link.springer.de/link/service/series/0558/bibs/2064/20640030%
195: .htm}
196: \BIBentrySTDinterwordspacing
197:
198: \bibitem{Men05}
199: \BIBentryALTinterwordspacing
200: V.~Ménissier-Morain, ``Arbitrary precision real arithmetic: design and
201: algorithms,'' \emph{Journal of Logic and Algebraic Programming}, vol.~64,
202: no.~1, pp. 13--39, 2005. [Online]. Available:
203: \url{http://dx.doi.org/10.1016/j.jlap.2004.07.003}
204: \BIBentrySTDinterwordspacing
205:
206: \bibitem{CiaDiG06}
207: \BIBentryALTinterwordspacing
208: A.~Ciaffaglione and P.~Di~Gianantonio, ``A certified, corecursive
209: implementation of exact real numbers,'' \emph{Theoretical Computer Science},
210: vol. 351, no.~1, pp. 39--51, 2006. [Online]. Available:
211: \url{http://dx.doi.org/10.1016/j.tcs.2005.09.061}
212: \BIBentrySTDinterwordspacing
213:
214: \bibitem{HugNiq06}
215: \BIBentryALTinterwordspacing
216: J.~Hughes and M.~Niqui, ``Admissible digit sets,'' \emph{Theoretical Computer
217: Science}, vol. 351, no.~1, pp. 61--73, 2006. [Online]. Available:
218: \url{http://dx.doi.org/10.1016/j.tcs.2005.09.059}
219: \BIBentrySTDinterwordspacing
220:
221: \bibitem{Dut96}
222: \BIBentryALTinterwordspacing
223: B.~Dutertre, ``Elements of mathematical analysis in {PVS},'' in \emph{Theorem
224: Proving in Higher Order Logics: 9th International Conference. TPHOLs'97},
225: ser. Lecture Notes in Computer Science, J.~von Wright, J.~Grundy, , and
226: J.~Harrison, Eds., no. 1125.\hskip 1em plus 0.5em minus 0.4em\relax Turku,
227: Finland: Springer-Verlag, August 1996, pp. 141--156. [Online]. Available:
228: \url{http://www.sdl.sri.com/papers/tphol96/}
229: \BIBentrySTDinterwordspacing
230:
231: \bibitem{DauMel04}
232: \BIBentryALTinterwordspacing
233: M.~Daumas and G.~Melquiond, ``Generating formally certified bounds on values
234: and round-off errors,'' in \emph{Real Numbers and Computers}, Dagstuhl,
235: Germany, 2004, pp. 55--70. [Online]. Available:
236: \url{http://hal.inria.fr/inria-00070739}
237: \BIBentrySTDinterwordspacing
238:
239: \bibitem{BolMun06}
240: \BIBentryALTinterwordspacing
241: S.~Boldo and C.~Muñoz, ``Provably faithful evaluation of polynomials,'' in
242: \emph{Proceedings of the 2006 ACM Symposium on Applied Computing}, Dijon,
243: France, 2006, pp. 1328--1332. [Online]. Available:
244: \url{http://doi.acm.org/10.1145/1141277.1141586}
245: \BIBentrySTDinterwordspacing
246:
247: \bibitem{LG02}
248: D.~Lester and P.~Gowland, ``Using {PVS} to validate the algorithms of an exact
249: arithmetic,'' \emph{Theoretical Computer Science}, vol. 291, no.~2, pp.
250: 203--218, Nov. 2002.
251:
252: \bibitem{MakBer03}
253: \BIBentryALTinterwordspacing
254: K.~Makino and M.~Berz, ``Taylor models and other validated functional inclusion
255: methods,'' \emph{International Journal of Pure and Applied Mathematics},
256: vol.~4, no.~4, pp. 379--456, 2003. [Online]. Available:
257: \url{http://bt.pa.msu.edu/pub/papers/TMIJPAM03/TMIJPAM03.pdf}
258: \BIBentrySTDinterwordspacing
259:
260: \bibitem{ChaDau06}
261: \BIBentryALTinterwordspacing
262: F.~Ch\'aves and M.~Daumas, ``A library to {T}aylor models for {PVS} automatic
263: proof checker,'' in \emph{Proceedings of the NSF workshop on reliable
264: engineering computing}, Savannah, Georgia, 2006, pp. 39--52. [Online].
265: Available:
266: \url{http://www.gtsav.gatech.edu/workshop/rec06/papers/Chaves_paper.pdf}
267: \BIBentrySTDinterwordspacing
268:
269: \bibitem{ChaDauMunRev07}
270: \BIBentryALTinterwordspacing
271: F.~Cháves, M.~Daumas, C.~Muñoz, and N.~Revol, ``Automatic strategies to
272: evaluate formulas on {T}aylor models and generate proofs in {PVS},'' in
273: \emph{6th International Congress on Industrial and Applied Mathematics},
274: Zurich, Switzerland, 2007. [Online]. Available: \url{http://www.iciam07.ch/}
275: \BIBentrySTDinterwordspacing
276:
277: \end{thebibliography}
278: