zbMATH — the first resource for mathematics

Polynomial function intervals for floating-point software verification. (English) Zbl 1296.65071
Summary: 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.
65G20 Algorithms with automatic result verification
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
65G30 Interval and finite arithmetic
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
65Y04 Numerical algorithms for computer arithmetic, etc.
65-04 Software, source code, etc. for problems pertaining to numerical analysis
Full Text: DOI
[1] Ada Reference Manual, ISO/IEC 8652:2007(E) Ed. 3. Ada Europe (2007). 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, LC, Metitarski: an automatic theorem prover for real-valued special functions, J. Autom. Reason., 44, 175-205, (2010) · Zbl 1215.68206
[4] Amey, P.: Correctness by construction: better can also be cheaper. CrossTalk Mag. 24-28 (2002) · Zbl 1126.65309
[5] Barnes, J, The spark way to correctness is via abstraction, Ada Lett., XX, 69-79, (2000)
[6] Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security, 2 edn. Addison-Wesley, London and Boston (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, 91-102, (2009), Rhodos · Zbl 1248.65045
[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 (2013). http://hal.inria.fr/hal-00790071 · Zbl 1225.68073
[10] Boldo, S., Filliâ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, Berlin (2009). doi:10.1007/978-3-642-02614-0_10 · Zbl 1247.68232
[11] Boldo, S., Lelay, C., Melquiond, G.: Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. In: Hawblitzel, C., Miller, D. (eds.) Proceedings of the The Second International Conference on Certified Programs and Proofs. Lecture Notes in Computer Science, vol. 7679, pp. 289-304.Kyoto, Japan (2012) . doi:10.1007/978-3-642-35308-6_22. http://hal.inria.fr/hal-00712938 · Zbl 1383.68070
[12] Cousot, P; Cousot, R; Feret, J; Mauborgne, L; Miné, A; Monniaux, D; Rival, X; Sagiv, S (ed.), The ASTREé analyzer, 21-30, (2005), Berlin · Zbl 1108.68422
[13] Cuoq, P; Kirchner, F; Kosmatov, N; Prevosto, V; Signoles, J; Yakobowski, B, Frama-c: a software analysis perspective, 233-247, (2012), Berlin
[14] Daumas, M; Melquiond, G, Certification of bounds on expressions involving rounded operators, ACM Trans. Math. Softw., 37, 1-20, (2010) · Zbl 1364.68328
[15] Delmas, D; Goubault, E; Putot, S; Souyris, J; Tekkal, K; Védrine, F, Towards an industrial use of fluctuat on safety-critical avionics software, 53-69, (2009), Berlin
[16] Duracz, J.: Verification of floatin point programs. Ph.D. thesis, Aston University (2010)
[17] Duracz, J., Konečný, M.: PolyPaver development portal. http://code.google.com/p/polypaver/. Accessed 28 April 2013
[18] Duracz, J.A., Farjudian, A., Konečný, M.: Enclosure constraints for floating point software verification. In: Proceedings of CFV 2009 in Grenoble (2009) · Zbl 1215.68206
[19] Duracz, J.A., Konečný, M.: Polynomial function enclosures and floating point software verification. In: Proceedings of CFV 2008 in Sydney, pp 56-67 (2008) · Zbl 0419.65031
[20] Filliâtre, JC; Paskevich, A, Why3-where programs meet provers, (2013), Rome
[21] Fränzle, M; Herde, C; Teige, T; Ratschan, S; Schubert, T, Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure, J. Satisf. Boolean Model. Comput., 1, 209-236, (2007) · Zbl 1144.68371
[22] Goubault, E; Putot, S; Yi, K (ed.), Static analysis of numerical algorithms, 18-34, (2006), Berlin · Zbl 1225.68073
[23] Granvilliers, L., Benhamou, F.: Algorithm 852: RealPaver: an interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. 32(1) (2006). http://www.lina.sciences.univ-nantes.fr/Publications/2006/GB06 · Zbl 1346.65020
[24] Kaucher, E, Interval analysis in the extended interval space ir, Comput. Suppl., 2, 33-49, (1980) · Zbl 0427.65031
[25] Makino, K., Berz, M.: Efficient control of the dependency problem based on taylor model methods. Reliab. Comput. 5, 3-12(10) (1999). http://www.ingentaconnect. com/content/klu/reom/1999/00000005/00000001/00204749 · Zbl 0936.65073
[26] Mason, J.C., Handscomb, D.C.: Chebyshev Polynomials. CRC Press, Boca Raton (2002)
[27] Neher, M; Jackson, KR; Nedialkov, NS, On Taylor model based integration of odes, SIAM J. Numer. Anal., 45, 236-262, (2007) · Zbl 1141.65056
[28] Neumaier, A, Taylor forms-use and limits, Reliab. Comput., 9, 43-79, (2003) · Zbl 1071.65070
[29] Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999) · Zbl 0932.68013
[30] Owre, S; Rushby, JM; Shankar, N; Kapur, D (ed.), PVS: a prototype verification system, 748-752, (1992), Saratoga
[31] ProVal team: Proval web portal. http://proval.lri.fr/index.en.html. Accessed 1 Sept 2011 (2011)
[32] Putot, S; Goubault, E; Martel, M, Static analysis-based validation of floating-point computations, LNCS, 2991, 306-313, (2004) · Zbl 1126.65309
[33] Ratschan, S, Efficient solving of quantified inequality constraints over the real numbers, ACM Trans. Comput. Logic, 7, 723-748, (2006) · Zbl 1367.68270
[34] Ratschan, S., et al.: RSolver. http://rsolver.sourceforge.net. Software Package (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.