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)


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.


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



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.


  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. (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). 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). 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). 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). 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). 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.
  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). 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).
  15. 15.
    Hatton, L., Roberts, A.: How accurate is scientific software? IEEE Trans. Softw. Eng. 20(10), 785–797 (1994). 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.
  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.
  19. 19.
    LeVeque, R.: Finite Difference Methods for Ordinary and Partial Differential Equations. Society for Industrial and Applied Mathematics (2007).
  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). 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.
  22. 22.
    Munson, T.: Mesh shape-quality optimization using the inverse mean-ratio metric. Math. Program. 110(3), 561–590 (2007). 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.
  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. 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).
  29. 29.
    Schwartz, J.T.: Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27(4), 701–717 (1980). 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).
  31. 31.
    Stein, W., Joyner, D.: SAGE: system for algebra and geometry experimentation. SIGSAM Bull. 39(2), 61–64 (2005). 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).
  33. 33.
    Wikipedia. Sylvester’s criterion. Accessed 31 Jan 2018.
  34. 34.
    Wolfram, S.: The Mathematica Book, 5th Edn. Wolfram Media Inc, Champaign (2003).
  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). 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