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 programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs.
  • 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