{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,15]],"date-time":"2025-07-15T03:44:59Z","timestamp":1752551099881},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242970"},{"type":"electronic","value":"9783540305798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_4","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"59-77","source":"Crossref","is-referenced-by-count":17,"title":["An Overview of Semantics for the Validation of Numerical Programs"],"prefix":"10.1007","author":[{"given":"Matthieu","family":"Martel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/b97589","volume-title":"Chaos, an Introduction to Dynamical Systems","author":"K.T. Alligood","year":"1996","unstructured":"Alligood, K.T., Sauer, T.D., Yorke, J.A.: Chaos, an Introduction to Dynamical Systems. Springer, Heidelberg (1996)"},{"key":"4_CR2","unstructured":"ANSI\/IEEE. IEEE Standard for Binary Floating Point Arithmetic, Std 754 edn. (1985)"},{"key":"4_CR3","volume-title":"Partial Evaluation and Semantics-Based Program Transformations, PEPM 2002","author":"C. Bischof","year":"2002","unstructured":"Bischof, C., Hovland, P.D., Norris, B.: Implementation of automatic differentiation tools. In: Partial Evaluation and Semantics-Based Program Transformations, PEPM 2002. ACM Press, New York (2002)"},{"key":"4_CR4","volume-title":"Programming Language Design and Implementation, PLDI 2003","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation, PLDI 2003. ACM Press, New York (2003)"},{"key":"4_CR5","volume-title":"Symposium on Computer Arithmetic","author":"S. Boldo","year":"2003","unstructured":"Boldo, S., Daumas, M.: Representable correcting terms for possibly underflowing floating point operations. In: Bajard, J.-C., Schulte, M. (eds.) Symposium on Computer Arithmetic. IEEE Press, Los Alamitos (2003)"},{"key":"4_CR6","unstructured":"Bronnimann, H., Melquiond, G.: The boost interval arithmetic library. In: Real Numbers and Computers Conference, RNC\u20195 (2003)"},{"key":"4_CR7","unstructured":"CADNA for C\/C++ source codes User\u2019s Guide, http:\/\/www-anp.lip6.fr\/cadna\/Documentation\/Accueil.php"},{"key":"4_CR8","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719673","volume-title":"Lectures on Finite Precision Computations","author":"F. Chaitin-Chatelin","year":"1996","unstructured":"Chaitin-Chatelin, F., Frayss\u00e9, V.: Lectures on Finite Precision Computations. SIAM, Philadelphia (1996)"},{"key":"4_CR9","unstructured":"Chesneaux, J.-M.: L\u2019arithm\u00e9tique stochastique et le logiciel CADNA. Habilitation \u00e0 diriger des recherches, Universit\u00e9 Pierre et Marie Curie, Paris (1995)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-44755-5_13","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Daumas","year":"2001","unstructured":"Daumas, M., Rideau, L., Th\u00e9ry, L.: A generic library for floating-point numbers and its application to exact computing. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, p. 169. Springer, Heidelberg (2001)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Goldberg, D.: What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys\u00a023(1) (1991)","DOI":"10.1145\/103162.103163"},{"key":"4_CR12","volume-title":"Matrix Computations","author":"G.H. Golub","year":"1990","unstructured":"Golub, G.H., Van Loan, C.F.: Matrix Computations, 2nd edn. The Johns Hopkins University Press, Baltimore (1990)","edition":"2"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-47764-0_14","volume-title":"Static Analysis","author":"E. Goubault","year":"2001","unstructured":"Goubault, E.: Static analyses of the precision of floating-point operations. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, p. 234. Springer, Heidelberg (2001)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45927-8_15","volume-title":"Programming Languages and Systems","author":"E. Goubault","year":"2002","unstructured":"Goubault, E., Martel, M., Putot, S.: Asserting the precision of floating-point computations: a simple abstract interpreter. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 209\u2013212. Springer, Heidelberg (2002)"},{"key":"4_CR15","series-title":"Frontiers in Applied Mathematics","volume-title":"Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation","author":"A. Griewank","year":"2000","unstructured":"Griewank, A.: Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation. Frontiers in Applied Mathematics. SIAM, Philadelphia (2000)"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/229473.229474","volume":"22","author":"A. Griewank","year":"1996","unstructured":"Griewank, A., Juedes, D., Utke, J.: ADOL-C, a package for the automatic differentiation of algorithms written in c\/c++. ACM Trans. Math. Software\u00a022, 131\u2013167 (1996)","journal-title":"ACM Trans. Math. Software"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-24738-8_4","volume-title":"Numerical Software with Result Verification","author":"M. Grimmer","year":"2004","unstructured":"Grimmer, M., Petras, K., Revol, N.: Multiple precision interval packages: Comparing different approaches. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Dagstuhl Seminar 2003. LNCS, vol.\u00a02991, pp. 64\u201390. Springer, Heidelberg (2004)"},{"key":"4_CR18","unstructured":"Hanrot, G., Lefevre, V., Rouillier, F., Zimmermann, P.: The MPFR library. Institut de Recherche en Informatique et Automatique (2001)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1999","unstructured":"Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, p. 113. Springer, Heidelberg (1999)"},{"issue":"3","key":"4_CR20","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1023\/A:1021919329342","volume":"41","author":"P. Langlois","year":"2001","unstructured":"Langlois, P.: Automatic linear correction of rounding errors. BIT, Numerical Mathematics\u00a041(3), 515\u2013539 (2001)","journal-title":"BIT, Numerical Mathematics"},{"key":"4_CR21","unstructured":"Langlois, P., Nativel, F.: Improving automatic reduction of round-off errors. In: IMACS World Congress on Scientific Computation, Modelling and Applied Mathematics, vol.\u00a02 (1997)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-45927-8_14","volume-title":"Programming Languages and Systems","author":"M. Martel","year":"2002","unstructured":"Martel, M.: Propagation of roundoff errors in finite precision computations: a semantics approach. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 194\u2013208. Springer, Heidelberg (2002)"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-45789-5_12","volume-title":"Static Analysis","author":"M. Martel","year":"2002","unstructured":"Martel, M.: Static analysis of the numerical stability of loops. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, p. 133. Springer, Heidelberg (2002)"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/3-540-45578-7_36","volume-title":"Principles and Practice of Constraint Programming - CP 2001","author":"C. Michel","year":"2001","unstructured":"Michel, C., Rueher, M., Lebbah, Y.: Solving constraints over floating-point numbers. In: Walsh, T. (ed.) CP 2001. LNCS, vol.\u00a02239, p. 524. Springer, Heidelberg (2001)"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45099-3_17","volume-title":"Static Analysis","author":"D. Monniaux","year":"2000","unstructured":"Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 322\u2013340. Springer, Heidelberg (2000)"},{"key":"4_CR26","volume-title":"Principles of Programming Languages, POPL 2001","author":"D. Monniaux","year":"2001","unstructured":"Monniaux, D.: An abstract Monte-Carlo method for the analysis of probabilistic programs. In: Principles of Programming Languages, POPL 2001. ACM Press, New York (2001)"},{"key":"4_CR27","doi-asserted-by":"crossref","DOI":"10.1137\/1.9781611970906","volume-title":"Methods and Applications of Interval Analysis","author":"R.E. Moore","year":"1979","unstructured":"Moore, R.E.: Methods and Applications of Interval Analysis. SIAM, Philadelphia (1979)"},{"key":"4_CR28","volume-title":"Procs. of Logic in Computer Science","author":"P.J. Potts","year":"1997","unstructured":"Potts, P.J., Edalat, A., Escard\u00f3, H.M.: Semantics of exact real arithmetic. In: Procs. of Logic in Computer Science. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"4_CR29","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1109\/ARITH.1991.145549","volume-title":"Symposium on Computer Arithmetic","author":"M. Priest","year":"1991","unstructured":"Priest, M.: Algorithms for arbitrary precision floating point arithmetic. In: Kornerup, P., Matula, D. (eds.) Symposium on Computer Arithmetic, pp. 132\u2013144. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"4_CR30","unstructured":"Revol, N., Rouillier, F.: Motivations for an arbitrary precision interval arithmetic and the MPFI library. Technical Report RR-200227, Laboratoire de l\u2019Informatique du Parall\u00e9lisme, ENS-Lyon, France (2002)"},{"issue":"3","key":"4_CR31","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/0378-4754(93)90003-D","volume":"35","author":"J. Vignes","year":"1993","unstructured":"Vignes, J.: A stochastic arithmetic for reliable scientific computation. Mathematics and Computers in Simulation\u00a035(3), 233\u2013261 (1993)","journal-title":"Mathematics and Computers in Simulation"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:24:19Z","timestamp":1605759859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}