Abstract
The use of real numbers in a program can introduce differences between the expected and the actual behavior of the program, due to the finite representation of these numbers. Therefore, one may want to define programs using real numbers such that this difference vanishes. This paper defines a program transformation for a certain class of programs that improves the accuracy of the computations on real number representations by removing the square root and division operations from the original program in order to enable exact computation with addition, multiplication and subtraction. This transformation is meant to be used on embedded systems, therefore the produced programs have to respect constraints relative to this kind of code. In order to ensure that the transformation is correct, i.e., preserves the semantics, we also aim at specifying and proving this transformation using the PVS proof assistant.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Boldo, S., Filliâtre, J.-C.: Formal verification of floating-point programs. In: Kornerup, P., Muller, J.-M. (eds.) Proceedings of the 18th IEEE Symposium on Computer Arithmetic, Montpellier, France, pp. 187–194 (June 2007)
Boldo, S., Muñoz, C.: A formalization of floating-point numbers in PVS. Report NIA Report No. 2006-01, NASA/CR-2006-214298, NIA-NASA Langley, National Institute of Aerospace, Hampton, VA (2006)
Bostan, A.: Algorithmique efficace pour des opérations de base en Calcul formel. Ph.d. thesis (2003), http://algo.inria.fr/bostan/these/These.pdf
Chen, L., Miné, A., Cousot, P.: A Sound Floating-Point Polyhedra Abstract Domain. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 3–18. Springer, Heidelberg (2008)
Cohen, C.: Construction of Real Algebraic Numbers in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 67–82. Springer, Heidelberg (2012)
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. SIGSAM Bull 10, 10–12 (1976)
Daumas, M., Melquiond, G., Muñoz, C.: Guaranteed proofs using interval arithmetic. In: IEEE Symposium on Computer Arithmetic, pp. 188–195 (2005)
Harrison, J.: Floating Point Verification in HOL. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971, pp. 186–199. Springer, Heidelberg (1995)
IEEE. IEEE standard for binary floating-point arithmetic. Institute of Electrical and Electronics Engineers, New York, Note: Standard 754–1985 (1985)
Maddalon, J., Butler, R., Muñoz, C., Dowek, G.: Mathematical basis for the safety analysis of conflict prevention algorithms. Technical Memorandum NASA/TM-2009-215768, NASA, Langley Research Center, Hampton VA 23681-2199, USA (June 2009)
Martel, M.: Program transformation for numerical precision. In: PEPM, pp. 101–110 (2009)
Miner, P.S.: Defining the ieee-854 floating-point standard in pvs (1995)
Narkawicz, A., Muñoz, C., Dowek, G.: Formal verification of air traffic prevention bands algorithms. Technical Memorandum NASA/TM-2010-216706, NASA, Langley Research Center, Hampton VA 23681-2199, USA (June 2010)
Neron, P.: A formal proof of square root and division elimination in embedded programs - long version (2012), http://www.lix.polytechnique.fr/~neron/
Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. Univ. of California Press (1951)
Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997)
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
Neron, P. (2012). A Formal Proof of Square Root and Division Elimination in Embedded Programs. In: Hawblitzel, C., Miller, D. (eds) Certified Programs and Proofs. CPP 2012. Lecture Notes in Computer Science, vol 7679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35308-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-35308-6_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35307-9
Online ISBN: 978-3-642-35308-6
eBook Packages: Computer ScienceComputer Science (R0)