{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:16:13Z","timestamp":1784232973721,"version":"3.55.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319997247","type":"print"},{"value":"9783319997254","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99725-4_14","type":"book-chapter","created":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T13:45:50Z","timestamp":1535550350000},"page":"205-222","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Properties of Differentiable Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3479-6361","authenticated-orcid":false,"given":"Jan","family":"H\u00fcckelheim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ziqing","family":"Luo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sri Hari Krishna","family":"Narayanan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephen","family":"Siegel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul D.","family":"Hovland","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,8,29]]},"reference":[{"key":"14_CR1","unstructured":"Maplesoft: a division of Waterloo Maple Inc., Maple 18 (2014)"},{"key":"14_CR2","unstructured":"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)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, R., et al.: Templates for the Solution of Linear Systems: Building Blocks for Iterative Methods, vol. 43. SIAM (1994)","DOI":"10.1137\/1.9781611971538"},{"issue":"1","key":"14_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1055531.1055532","volume":"31","author":"P Bientinesi","year":"2005","unstructured":"Bientinesi, P., Gunnels, J.A., Myers, M.E., Quintana-Ort\u00ed, E.S., van de Geijn, R.A.: The science of deriving dense linear algebra algorithms. ACM Trans. Math. Softw. 31(1), 1\u201326 (2005). https:\/\/doi.org\/10.1145\/1055531.1055532","journal-title":"ACM Trans. Math. Softw."},{"issue":"3","key":"14_CR6","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/j.camwa.2014.06.004","volume":"68","author":"S Boldo","year":"2014","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00edtre, 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\u2013352 (2014). https:\/\/doi.org\/10.1016\/j.camwa.2014.06.004","journal-title":"Comput. Math. Appl."},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"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\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Eijkhout, V., Bientinesi, P., van de Geijn, R.: Towards mechanical derivation of krylov solver libraries. Procedia Comput. Sci. 1(1), 1805\u20131813 (2010). ICCS 2010. https:\/\/doi.org\/10.1016\/j.procs.2010.04.202","DOI":"10.1016\/j.procs.2010.04.202"},{"issue":"2","key":"14_CR10","doi-asserted-by":"publisher","first-page":"435","DOI":"10.5194\/gmd-4-435-2011","volume":"4","author":"PE Farrell","year":"2011","unstructured":"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\u2013449 (2011). https:\/\/doi.org\/10.5194\/gmd-4-435-2011","journal-title":"Geosci. Model Dev."},{"issue":"184","key":"14_CR11","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1090\/S0025-5718-1988-0935077-0","volume":"51","author":"B Fornberg","year":"1988","unstructured":"Fornberg, B.: Generation of finite difference formulas on arbitrarily spaced grids. Math. Comput. 51(184), 699\u2013706 (1988)","journal-title":"Math. Comput."},{"key":"14_CR12","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-oriented Software (1995)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Gopalakrishnan, G., et al.: Report of the HPC correctness summit, 25\u201326 Jan 2017, Washington, DC. Technical report (2017)","DOI":"10.2172\/1470989"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Hasco\u00ebt, 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","DOI":"10.1145\/2450153.2450158"},{"issue":"10","key":"14_CR15","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.328993","volume":"20","author":"L Hatton","year":"1994","unstructured":"Hatton, L., Roberts, A.: How accurate is scientific software? IEEE Trans. Softw. Eng. 20(10), 785\u2013797 (1994). https:\/\/doi.org\/10.1109\/32.328993","journal-title":"IEEE Trans. Softw. Eng."},{"key":"14_CR16","unstructured":"Hoffman, J.D., Frankel, S.: Numerical Methods for Engineers and Scientists. CRC Press (2001)"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"H\u00fcckelheim, 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\u201349 (2017). ACM, New York. https:\/\/doi.org\/10.1145\/3145344.3145488","DOI":"10.1145\/3145344.3145488"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"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\u20131143 (2012). Accelerators for High-Performance Computing. https:\/\/doi.org\/10.1016\/j.jpdc.2011.10.014","DOI":"10.1016\/j.jpdc.2011.10.014"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.1137\/1.9780898717839"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-41071-0_5","volume-title":"Formal Methods: Foundations and Applications","author":"TB Marcilon","year":"2013","unstructured":"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\u201366. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41071-0_5"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Munson, T.S., Hovland, P.D.: The FeasNewt benchmark. In: IEEE International. 2005 Proceedings of the IEEE Workload Characterization Symposium 2005, pp. 150\u2013154, October 2005. https:\/\/doi.org\/10.1109\/IISWC.2005.1526011","DOI":"10.1109\/IISWC.2005.1526011"},{"issue":"3","key":"14_CR22","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/s10107-006-0014-3","volume":"110","author":"T Munson","year":"2007","unstructured":"Munson, T.: Mesh shape-quality optimization using the inverse mean-ratio metric. Math. Program. 110(3), 561\u2013590 (2007). https:\/\/doi.org\/10.1007\/s10107-006-0014-3","journal-title":"Math. Program."},{"key":"14_CR23","unstructured":"Munson, T.S.: Optimizing the quality of mesh elements. In: SIAG\/OPT Views-and-News, p. 27 (2005)"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"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\u20131853 (2010). ICCS 2010. https:\/\/doi.org\/10.1016\/j.procs.2010.04.206","DOI":"10.1016\/j.procs.2010.04.206"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Naumann, U.: The Art of Differentiating Computer Programs: An Introduction to Algorithmic Differentiation, vol. 24. SIAM (2012)","DOI":"10.1137\/1.9781611972078"},{"key":"14_CR26","unstructured":"Oracle. Java8: Class random (2017). https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/Random.html"},{"key":"14_CR27","unstructured":"SARL: The Symbolic Algebra and Reasoning Library. http:\/\/vsl.cis.udel.edu\/sarl . Accessed 31 Jan 2018"},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Schordan, M., H\u00fcckelheim, 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\u201341. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3145344.3145489","DOI":"10.1145\/3145344.3145489"},{"issue":"4","key":"14_CR29","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1145\/322217.322225","volume":"27","author":"JT Schwartz","year":"1980","unstructured":"Schwartz, J.T.: Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27(4), 701\u2013717 (1980). https:\/\/doi.org\/10.1145\/322217.322225","journal-title":"J. ACM"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"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\u201361:12. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2807591.2807635","DOI":"10.1145\/2807591.2807635"},{"issue":"2","key":"14_CR31","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/1101884.1101889","volume":"39","author":"W Stein","year":"2005","unstructured":"Stein, W., Joyner, D.: SAGE: system for algebra and geometry experimentation. SIGSAM Bull. 39(2), 61\u201364 (2005). https:\/\/doi.org\/10.1145\/1101884.1101889","journal-title":"SIGSAM Bull."},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"van de Vorst, J.G.G.: The formal development of a parallel program performing LU-decomposition. Acta Informatica 26(1), 1\u201317 (1988). https:\/\/doi.org\/10.1007\/BF02915443","DOI":"10.1007\/BF02915443"},{"key":"14_CR33","unstructured":"Wikipedia. Sylvester\u2019s criterion. Accessed 31 Jan 2018. https:\/\/en.wikipedia.org\/wiki\/Sylvester%27s_criterion"},{"key":"14_CR34","unstructured":"Wolfram, S.: The Mathematica Book, 5th Edn. Wolfram Media Inc, Champaign (2003). http:\/\/www.wolfram.com\/books\/profile.cgi?id=4939"},{"key":"14_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-09519-5_73","volume-title":"Symbolic and Algebraic Computation","author":"R Zippel","year":"1979","unstructured":"Zippel, R.: Probabilistic algorithms for sparse polynomials. In: Ng, E.W. (ed.) Symbolic and Algebraic Computation. LNCS, vol. 72, pp. 216\u2013226. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/3-540-09519-5_73"},{"key":"14_CR36","unstructured":"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)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99725-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T00:56:25Z","timestamp":1571792185000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99725-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319997247","9783319997254"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99725-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}