Abstract
The mathematical concept of real numbers is much richer than the double precision numbers widely used as their implementation on a computer. The field of ‘exact real arithmetic’ tries to combine the elegance and correctness of the mathematical theories with the speed of double precision hardware, as far as possible. In this paper, we describe an ongoing approach using the specification language ACSL, the tool suite Frama-C (with why and jessie) and the proof assistant Coq to verify central aspects of the iRRAM software package, which is known to be a fast C++ implementation of ‘exact’ reals numbers.
This work was partially supported by the DFG project 446 CHV 113/240/0-1.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bauer, A.: Efficient computation with Dedekind reals. In: 5th International Conference on Computability and Complexity in Analysis, CCA 2008, Hagen, Germany, August 21-24 (2008)
Bauer, A., Kavkler, I.: Implementing real numbers with rz. Electron. Notes Theor. Comput. Sci. 202, 365–384 (2008)
Brattka, V., Hertling, P., Weihrauch, K.: A Tutorial on Computable Analysis. In: Barry Cooper, S., Löwe, B., Sorbi, A. (eds.) New Computational Paradigms: Changing Conceptions of What is Computable, pp. 425–491. Springer, New York (2008)
Lambov, B.: Reallib: An efficient implementation of exact real arithmetic. Mathematical Structures in Computer Science 17(1), 81–98 (2007)
Lester, D.R.: The world’s shortest correct exact real arithmetic program? In: Proc. 8th Conference on Real Numbers and Computers, pp. 103–112 (2008)
Marché, C., Paulin-Mohring, C., Urbain, X.: The krakatoa tool for certification of java/javacard programs annotated in jml. J. Log. Algebr. Program. 58(1-2), 89–106 (2004)
Müller, N.T.: The iRRAM: Exact Arithmetic in C++. In: Blank, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 222–252. Springer, Heidelberg (2001)
O’Connor, R., Spitters, B.: A computer-verified monadic functional implementation of the integral. Theor. Comput. Sci. 411(37), 3386–3402 (2010)
Weihrauch, K.: Computable analysis: An introduction. Springer-Verlag New York, Inc. (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller, N.T., Uhrhan, C. (2012). Some Steps into Verification of Exact Real Arithmetic. In: Goodloe, A.E., Person, S. (eds) NASA Formal Methods. NFM 2012. Lecture Notes in Computer Science, vol 7226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28891-3_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-28891-3_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28890-6
Online ISBN: 978-3-642-28891-3
eBook Packages: Computer ScienceComputer Science (R0)