Advertisement

Verifying Properties of Differentiable Programs

  • Jan HückelheimEmail author
  • Ziqing Luo
  • Sri Hari Krishna Narayanan
  • Stephen Siegel
  • Paul D. Hovland
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

There is growing demand for formal verification methods in the scientific and high performance computing communities. For scientific applications, it is not only necessary to verify the absence of violations such as out of bounds access or race conditions, but also to ensure that the results satisfy certain mathematical properties. In this work, we explore the limits of automated bounded verification in the verification of these programs by applying the symbolic execution tool CIVL to some numerical algorithms that are frequently used in scientific programs, namely a conjugate gradient solver, a finite difference stencil, and a mesh quality metric. These algorithms implement differentiable functions, allowing us to use the automatic differentiation tools Tapenade and ADIC in the creation of their specifications.

Keywords

Formal verification Static analysis Symbolic execution Model checking Algorithmic differentiation Numerical algorithms 

Notes

Acknowledgements

This work was supported by the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research, Applied Mathematics and Computer Science programs under contract number DE-AC02-06CH11357 and contract number DE-SC0012566, and by U.S. National Science Foundation Award CCF-1319571. The authors thank Prof. Dan Roche of the U.S. Naval Academy and Prof. David Saunders of the Univ. of Delaware for their assistance with computer algebra and probabilistic approaches.

References

  1. 1.
    Maplesoft: a division of Waterloo Maple Inc., Maple 18 (2014)Google Scholar
  2. 2.
    Kozen, D., Barth, A.: Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests. Technical report, 10. http://hdl.handle.net/1813/5848 (2002)
  3. 3.
    Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_14CrossRefGoogle Scholar
  4. 4.
    Barrett, R., et al.: Templates for the Solution of Linear Systems: Building Blocks for Iterative Methods, vol. 43. SIAM (1994)Google Scholar
  5. 5.
    Bientinesi, P., Gunnels, J.A., Myers, M.E., Quintana-Ortí, E.S., van de Geijn, R.A.: The science of deriving dense linear algebra algorithms. ACM Trans. Math. Softw. 31(1), 1–26 (2005).  https://doi.org/10.1145/1055531.1055532MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Boldo, S., Clément, F., Filliítre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Trusting computations: a mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68(3), 325–352 (2014).  https://doi.org/10.1016/j.camwa.2014.06.004MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33826-7_16CrossRefGoogle Scholar
  8. 8.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  9. 9.
    Eijkhout, V., Bientinesi, P., van de Geijn, R.: Towards mechanical derivation of krylov solver libraries. Procedia Comput. Sci. 1(1), 1805–1813 (2010). ICCS 2010.  https://doi.org/10.1016/j.procs.2010.04.202
  10. 10.
    Farrell, P.E., Piggott, M.D., Gorman, G.J., Ham, D.A., Wilson, C.R., Bond, T.M.: Automated continuous verification for numerical simulation. Geosci. Model Dev. 4(2), 435–449 (2011).  https://doi.org/10.5194/gmd-4-435-2011CrossRefGoogle Scholar
  11. 11.
    Fornberg, B.: Generation of finite difference formulas on arbitrarily spaced grids. Math. Comput. 51(184), 699–706 (1988)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-oriented Software (1995)Google Scholar
  13. 13.
    Gopalakrishnan, G., et al.: Report of the HPC correctness summit, 25–26 Jan 2017, Washington, DC. Technical report (2017)Google Scholar
  14. 14.
    Hascoët, L., Pascual, V.: The tapenade automatic differentiation tool: principles, model, and specification. ACM Trans. Math. Softw. 39(3), (2013).  https://doi.org/10.1145/2450153.2450158
  15. 15.
    Hatton, L., Roberts, A.: How accurate is scientific software? IEEE Trans. Softw. Eng. 20(10), 785–797 (1994).  https://doi.org/10.1109/32.328993CrossRefGoogle Scholar
  16. 16.
    Hoffman, J.D., Frankel, S.: Numerical Methods for Engineers and Scientists. CRC Press (2001)Google Scholar
  17. 17.
    Hückelheim, J., et al.: Towards self-verification in finite difference code generation. In: Proceedings of the First International Workshop on Software Correctness for HPC Applications, Correctness 2017, pp. 42–49 (2017). ACM, New York.  https://doi.org/10.1145/3145344.3145488
  18. 18.
    Igual, F.D., et al.: The flame approach: from dense linear algebra algorithms to high-performance multi-accelerator implementations. J. Parallel Distrib. Comput. 72(9), 1134–1143 (2012). Accelerators for High-Performance Computing.  https://doi.org/10.1016/j.jpdc.2011.10.014
  19. 19.
    LeVeque, R.: Finite Difference Methods for Ordinary and Partial Differential Equations. Society for Industrial and Applied Mathematics (2007).  https://doi.org/10.1137/1.9780898717839
  20. 20.
    Marcilon, T.B., de Carvalho Junior, F.H.: Derivation and verification of parallel components for the needs of an HPC cloud. In: Iyoda, J., de Moura, L. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 51–66. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-41071-0_5CrossRefzbMATHGoogle Scholar
  21. 21.
    Munson, T.S., Hovland, P.D.: The FeasNewt benchmark. In: IEEE International. 2005 Proceedings of the IEEE Workload Characterization Symposium 2005, pp. 150–154, October 2005.  https://doi.org/10.1109/IISWC.2005.1526011
  22. 22.
    Munson, T.: Mesh shape-quality optimization using the inverse mean-ratio metric. Math. Program. 110(3), 561–590 (2007).  https://doi.org/10.1007/s10107-006-0014-3MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Munson, T.S.: Optimizing the quality of mesh elements. In: SIAG/OPT Views-and-News, p. 27 (2005)Google Scholar
  24. 24.
    Narayanan, S.H.K., Norris, B., Winnicka, B.: Adic2: development of a component source transformation system for differentiating C and C++. Procedia Comput. Sci. 1(1), 1845–1853 (2010). ICCS 2010.  https://doi.org/10.1016/j.procs.2010.04.206
  25. 25.
    Naumann, U.: The Art of Differentiating Computer Programs: An Introduction to Algorithmic Differentiation, vol. 24. SIAM (2012)Google Scholar
  26. 26.
  27. 27.
    SARL: The Symbolic Algebra and Reasoning Library. http://vsl.cis.udel.edu/sarl. Accessed 31 Jan 2018
  28. 28.
    Schordan, M., Hückelheim, J., Lin, P.-H., Menon, H.: Verifying the floating-point computation equivalence of manually and automatically differentiated code. In: Proceedings of the First International Workshop on Software Correctness for HPC Applications, Correctness 2017, pp. 34–41. ACM, New York (2017).  https://doi.org/10.1145/3145344.3145489
  29. 29.
    Schwartz, J.T.: Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27(4), 701–717 (1980).  https://doi.org/10.1145/322217.322225MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Siegel, S.F., et al.: CIVL: the concurrency intermediate verification language. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2015, pp. 61:1–61:12. ACM, New York (2015).  https://doi.org/10.1145/2807591.2807635
  31. 31.
    Stein, W., Joyner, D.: SAGE: system for algebra and geometry experimentation. SIGSAM Bull. 39(2), 61–64 (2005).  https://doi.org/10.1145/1101884.1101889CrossRefzbMATHGoogle Scholar
  32. 32.
    van de Vorst, J.G.G.: The formal development of a parallel program performing LU-decomposition. Acta Informatica 26(1), 1–17 (1988).  https://doi.org/10.1007/BF02915443
  33. 33.
    Wikipedia. Sylvester’s criterion. Accessed 31 Jan 2018. https://en.wikipedia.org/wiki/Sylvester%27s_criterion
  34. 34.
    Wolfram, S.: The Mathematica Book, 5th Edn. Wolfram Media Inc, Champaign (2003). http://www.wolfram.com/books/profile.cgi?id=4939
  35. 35.
    Zippel, R.: Probabilistic algorithms for sparse polynomials. In: Ng, E.W. (ed.) Symbolic and Algebraic Computation. LNCS, vol. 72, pp. 216–226. Springer, Heidelberg (1979).  https://doi.org/10.1007/3-540-09519-5_73CrossRefGoogle Scholar
  36. 36.
    Zirkel, T.K., Siegel, S.F., Rossi, L.F.: Using symbolic execution to verify the order of accuracy of numerical approximations. Technical report UD-CIS-2014/002, Department of Computer and Information Sciences, University of Delaware (2014)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Imperial College LondonLondonUK
  2. 2.University of DelawareNewarkUSA
  3. 3.Argonne National LaboratoryArgonneUSA

Personalised recommendations