Polynomial function intervals for floating-point software verification

Article English OPEN
Duracz, Jan ; Konečný, Michal (2014)

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such progr... View more
  • References (34)
    34 references, page 1 of 4

    1. Ada Reference Manual, ISO/IEC 8652:2007(E) Ed. 3. Ada Europe (2007). URL http://www.adaic. org/standards/05rm/html/RM-TTL.html

    2. Abramowitz, M., Stegun, I.A.: Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables, ninth dover printing, tenth gpo printing edn. Dover, New York (1964)

    3. Akbarpour, B., Paulson, L.C.: Metitarski: An automatic theorem prover for real-valued special functions. J. Autom. Reasoning 44(3), 175-205 (2010)

    4. Amey, P.: Correctness by construction: Better can also be cheaper. CrossTalk Magazine pp. 24-28 (2002)

    5. Barnes, J.: The spark way to correctness is via abstraction. Ada Lett. XX(4), 69-79 (2000). DOI http://doi.acm.org/10.1145/369264.369271

    6. Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security, 2 edn. AddisonWesley (2003)

    7. Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the tokeneer enclave protection software. In: Proceedings of IEEE International Symposium on Secure Software Engineering (2006)

    8. Boldo, S.: Floats & Ropes: a case study for formal numerical program verification. In: 36th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science - ARCoSS, vol. 5556, pp. 91-102. Springer, Rhodos, Greece (2009)

    9. Boldo, S.: How to compute the area of a triangle: a formal revisit. In: Proceedings of the 21th IEEE Symposium on Computer Arithmetic. Austin, Texas, USA (2013). URL http://hal.inria.fr/ hal-00790071

    10. Boldo, S., Filliaˆtre, J.C., Melquiond, G.: Combining coq and gappa for certifying floating-point programs. In: Calculemus '09/MKM '09: Proceedings of the 16th Symposium, 8th International Conference. Held as Part of CICM '09 on Intelligent Computer Mathematics, pp. 59-74. Springer-Verlag, Berlin, Heidelberg (2009). DOI http://dx.doi.org/10.1007/978-3-642-02614-0 10

  • Metrics
    views in OpenAIRE
    views in local repository
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    Aston Publications Explorer - IRUS-UK 0 21
Share - Bookmark