Formal verification of numerical programs: from C annotated programs to mechanical proofs. (English) Zbl 1264.68054
Summary: Numerical programs may require a high level of guarantee. This can be achieved by applying formal methods, such as machine-checked proofs. But these tools handle mathematical theorems while we are interested in C code, in which numerical computations are performed using floating-point arithmetic, whereas proof tools typically handle exact real arithmetic. To achieve this high level of confidence on C programs, we use a chain of tools: Frama-C, its Jessie plugin, Why and provers among Coq, Gappa, Alt-Ergo, CVC3 and Z3.
This approach requires the C program to be annotated: each function must be precisely specified, and we prove the correctness of the program by proving both that it meets its specifications and that no runtime error may occur. The purpose of this paper is to illustrate, on various examples, the features of this approach.
This approach requires the C program to be annotated: each function must be precisely specified, and we prove the correctness of the program by proving both that it meets its specifications and that no runtime error may occur. The purpose of this paper is to illustrate, on various examples, the features of this approach.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N15 | Theory of programming languages |
| 65Y04 | Numerical algorithms for computer arithmetic, etc. |
References:
| [1] | Ayad, A., Marché, C.: Multi-prover verification of floating-point programs. In: Giesl, J., Hähnle, R. (eds.) Fifth International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, Springer, Edinburgh (2010) · Zbl 1291.68321 |
| [2] | Barnett M., Leino K.R.M., Schulte W.: The spec# programming system: an overview. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS’04). Lecture Notes in Computer Science, vol. 3362, pp. 49-69. Springer, Berlin (2004) |
| [3] | Baudin, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language (2008). http://frama-c.cea.fr/acsl.html |
| [4] | Bertot Y., Castéran P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin (2004) · Zbl 1069.68095 |
| [5] | Boldo, S.: Preuves formelles en arithmétiques à virgule flottante. PhD thesis, École Normale Supérieure de Lyon (2004) |
| [6] | Boldo S.: Pitfalls of a full floating-point proof example on the formal proof of the Veltkamp/Dekker algorithms. In: Furbach, U., Shankar, N. (eds) Third International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, Seattle, USA, vol. 4130, pp. 52–66. Springer, Berlin (2006) · Zbl 1222.65156 |
| [7] | Boldo, S.: Floats & Ropes: a case study for formal numerical program verification. In: 36th International Colloquium on Automata, Languages and Programming, Rhodos, Greece. Lecture Notes in Computer Science–ARCoSS, vol. 5556, pp. 91–102. Springer, Berlin (2009) · Zbl 1248.65045 |
| [8] | Boldo S.: Kahan’s algorithm for a correct discriminant computation at last formally proven. IEEE Trans. Comput. 58(2), 220–225 (2009) · Zbl 1367.65206 · doi:10.1109/TC.2008.200 |
| [9] | Boldo, S., Clément, F., Filliâtre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Formal proof of a wave equation resolution scheme: the method error. In: Proceedings of the First Interactive Theorem Proving Conference, Edinburgh, Scotland. LNCS, Springer, Berlin (2010) · Zbl 1291.68329 |
| [10] | Boldo, S., Daumas, M., Kahan, W., Melquiond, G.: Proof and certification for an accurate discriminant. In: 12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg, Germany (2006) |
| [11] | Boldo, S., Filliâtre, J.-C.: Formal verification of floating-point programs. In: 18th IEEE International Symposium on Computer Arithmetic, Montpellier, France, pp. 187–194 (2007) |
| [12] | Boldo, S., Filliâtre, J.-C., Melquiond, G.: Combining Coq and Gappa for certifying floating-point programs. In: 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Grand Bend, Canada. Lecture Notes in Artificial Intelligence, vol. 5625, pp. 59–74. Springer, Berlin (2009) · Zbl 1247.68232 |
| [13] | Boldo, S., Nguyen, T.M.T.: Hardware-independent proofs of numerical programs. In: Muñoz, C. (ed.) Proceedings of the Second NASA Formal Methods Symposium. number NASA/CP-2010-216215 in NASA Conference Publication, Washington D.C., USA, pp. 14–23 (2010) |
| [14] | Boldo S., Nguyen T.M.T.: Proofs of numerical programs when the compiler optimizes. Innov. Syst. Softw. Eng 7, 1–10 (2011) · doi:10.1007/s11334-010-0138-8 |
| [15] | Burdy L., Cheon Y., Cok D.R., Ernst M.D., Kiniry J.R., Leavens G.T., Leino K.R.M., Poll E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. (STTT) 7(3), 212–232 (2005) · doi:10.1007/s10009-004-0167-4 |
| [16] | Carré, B., Garnsworthy, J.: SPARK–an annotated Ada subset for safety-critical programming. In: Proceedings of the Conference on TRI-ADA’90, TRI-Ada’90, pp. 392–402. ACM Press, New York (1990) |
| [17] | Carreño, V.A., Miner P.S.: Specification of the IEEE-854 floating-point standard in HOL and PVS. In: HOL95: 8th International Workshop on Higher-Order Logic Theorem Proving and Its Applications, Aspen Grove, UT (1995) |
| [18] | Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer. In: ESOP. Lecture Notes in Computer Science, vol. 3444, pp. 21–30 (2005) · Zbl 1108.68422 |
| [19] | Daumas M., Rideau L., Théry L.: A generic library of floating-point numbers and its application to exact computing. In: 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, pp. 169–184 (2001) · Zbl 1005.68544 |
| [20] | Dekker T.J.: A floating point technique for extending the available precision. Numerische Mathematik 18(3), 224–242 (1971) · Zbl 0226.65034 · doi:10.1007/BF01397083 |
| [21] | Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: FMICS, LNCS, vol. 5825, pp. 53–69. Springer, Berlin (2009) |
| [22] | Filliâtre J.-C., Marché C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds) 19th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590, pp. 173–177. Springer, Berlin (2007) |
| [23] | Gerlach, J., Burghardt, J.: An experience report on the verification of algorithms in the c++ standard library using frama-c. In: Beckert, B., Marché, C. (eds.) Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Karlsruhe Reports in Informatics, pp. 191–204. Paris, France, June (2010). http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083 |
| [24] | Goubault E., Putot S.: Static analysis of numerical algorithms. In: Yi, K. (eds) SAS. LNCS, vol. 4134, pp. 18–34. Springer, Berlin (2006) · Zbl 1225.68073 |
| [25] | Harrison, J.: Formal verification of floating point trigonometric functions. In: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, Austin, Texas, pp. 217–233 (2000) |
| [26] | Higham, N.J.: Accuracy and stability of numerical algorithms, 2nd edn, xxx+680 pp. SIAM, Philadelphia (2002). http://www.maths.manchester.ac.uk/\(\sim\)higham/asna/ · Zbl 1011.65010 |
| [27] | IEEE.: IEEE Standard for Floating-Point Arithmetic. IEEE Std. 754-2008 (2008) · Zbl 1143.76549 |
| [28] | Kahan, W.: On the cost of Floating-Point Computation Without Extra-Precise Arithmetic. World-Wide Web document, Nov. (2004) |
| [29] | Leavens G.T.: Not a number of floating point problems. J. Object Technol. 5(2), 75–83 (2006) · doi:10.5381/jot.2006.5.2.c8 |
| [30] | Melquiond, G.: Floating-point arithmetic in the Coq system. In: Proceedings of the 8th Conference on Real Numbers and Computers, pp. 93–102. Santiago de Compostela, Spain (2008) |
| [31] | Melquiond, G.: Proving bounds on real-valued functions with computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning, Sydney, Australia. Lecture Notes in Artificial Intelligence, vol. 5195, pp. 2–17 (2008) · Zbl 1165.68464 |
| [32] | Monniaux, D.: Analyse statique : de la théorie à la pratique. Habilitation to direct research Université Joseph Fourier, Grenoble, France (2009) |
| [33] | Moy, Y., Marché, C.: Jessie Plugin Tutorial, Beryllium version. INRIA (2009). http://www.frama-c.cea.fr/jessie.html |
| [34] | Moy Y., Marché C.: Modular inference of subprogram contracts for safety checking. J. Symb. Comput. 45, 1184–1211 (2010) · Zbl 1213.68385 · doi:10.1016/j.jsc.2010.06.004 |
| [35] | Necula, G.C., McPeak, S., Rahul, S.P., Weime, W.: Cil: Intermediate language and tools for analysis and transformation of c programs. In: Conference on Compiler Construction (CC’02) (2002) · Zbl 1051.68756 |
| [36] | Russinoff D.M.: A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS J. Comput. Math. 1, 148–200 (1998) · Zbl 0910.68008 · doi:10.1112/S1461157000000176 |
| [37] | Sterbenz P.H.: Floating Point Computation. Prentice Hall, Upper Saddle River (1974) |
| [38] | Veltkamp, G.W.: Algolprocedures voor het berekenen van een inwendig product in dubbele precisie. RC-Informatie 22, Technische Hogeschool Eindhoven (1968) |
| [39] | Wilkinson, J.H.: Rounding Errors in Algebraic Processes. Prentice-Hall, Upper Saddle River, NJ 07458, USA (1963) · Zbl 1041.65502 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
