{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T07:08:51Z","timestamp":1768028931264,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":60,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540343042","type":"print"},{"value":"9783540343059","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11757283_8","type":"book-chapter","created":{"date-parts":[[2006,11,27]],"date-time":"2006-11-27T13:02:12Z","timestamp":1164632532000},"page":"211-242","source":"Crossref","is-referenced-by-count":38,"title":["Floating-Point Verification Using Theorem Proving"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","year":"2000","unstructured":"Aagaard, M.D., Harrison, J. (eds.): TPHOLs 2000. LNCS, vol.\u00a01869. Springer, Heidelberg (2000)"},{"key":"8_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04315-8","volume-title":"Proofs from The Book","author":"M. Aigner","year":"2001","unstructured":"Aigner, M., Ziegler, G.M.: Proofs from The Book, 2nd edn. Springer, Heidelberg (2001)","edition":"2"},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","volume":"82","author":"K. Appel","year":"1976","unstructured":"Appel, K., Haken, W.: Every planar map is four colorable. Bulletin of the American Mathematical Society\u00a082, 711\u2013712 (1976)","journal-title":"Bulletin of the American Mathematical Society"},{"key":"8_CR4","volume-title":"A Concise Introduction to the Theory of Numbers","author":"A. Baker","year":"1985","unstructured":"Baker, A.: A Concise Introduction to the Theory of Numbers. Cambridge University Press, Cambridge (1985)"},{"key":"8_CR5","unstructured":"Boldo, S.: Preuves formelles en arithm\u00e9tiques \u00e0 virgule flottante. PhD thesis, ENS Lyon (2004), Available on the Web from: \n                  \n                    http:\/\/www.ens-lyon.fr\/LIP\/Pub\/Rapports\/PhD\/PhD2004\/PhD2004-05.pdf"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1145\/355972.355975","volume":"7","author":"W.S. Brown","year":"1981","unstructured":"Brown, W.S.: A simple but realistic model of floating-point computation. ACM Transactions on Mathematical Software\u00a07, 445\u2013480 (1981)","journal-title":"ACM Transactions on Mathematical Software"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098, 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the Simple Theory of Types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/62.322429","volume":"31","author":"C.W. Clenshaw","year":"1984","unstructured":"Clenshaw, C.W., Olver, F.W.J.: Beyond floating point. Journal of the ACM\u00a031, 319\u2013328 (1984)","journal-title":"Journal of the ACM"},{"key":"8_CR12","volume-title":"Scientific Computing for Itanium Based Systems","author":"M. Cornea","year":"2002","unstructured":"Cornea, M., Harrison, J., Tang, P.T.P.: Scientific Computing for Itanium Based Systems. Intel Press, Hillsboro (2002)"},{"key":"8_CR13","first-page":"1","volume":"Q2","author":"M. Cornea-Hasegan","year":"1998","unstructured":"Cornea-Hasegan, M.: Proving the IEEE correctness of iterative floating-point square root, divide and remainder algorithms. Intel Technology Journal\u00a01998-Q2, 1\u201311 (1998), available on the Web as: \n                  \n                    http:\/\/developer.intel.com\/technology\/itj\/q21998\/articles\/art_3.htm","journal-title":"Intel Technology Journal"},{"key":"8_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139173018","volume-title":"The Functional Approach to Programming","author":"G. Cousineau","year":"1998","unstructured":"Cousineau, G., Mauny, M.: The Functional Approach to Programming. Cambridge University Press, Cambridge (1998)"},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/BF01397083","volume":"18","author":"T.J. Dekker","year":"1971","unstructured":"Dekker, T.J.: A floating-point technique for extending the available precision. Numerical Mathematics\u00a018, 224\u2013242 (1971)","journal-title":"Numerical Mathematics"},{"issue":"7","key":"8_CR17","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/2.689674","volume":"64","author":"C. Dulong","year":"1998","unstructured":"Dulong, C.: The IA-64 architecture at work. IEEE Computer\u00a064(7), 24\u201332 (1998)","journal-title":"IEEE Computer"},{"key":"8_CR18","first-page":"194","volume":"5","author":"P. Erd\u00f6s","year":"1930","unstructured":"Erd\u00f6s, P.: Beweis eines Satzes von Tschebyshev. Acta Scientiarum Mathematicarum (Szeged)\u00a05, 194\u2013198 (1930)","journal-title":"Acta Scientiarum Mathematicarum (Szeged)"},{"key":"8_CR19","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1109\/DATE.2002.998262","volume-title":"Design, Automation and Test in Europe Conference and Exhibition (DATE 2002)","author":"E. Goldberg","year":"2002","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a fast and robust Sat-solver. In: Kloos, C.D., Franca, J.D. (eds.) Design, Automation and Test in Europe Conference and Exhibition (DATE 2002), Paris, France, pp. 142\u2013149. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"8_CR20","first-page":"163","volume-title":"Tools and notions for program construction: an advanced course","author":"M.J.C. Gordon","year":"1982","unstructured":"Gordon, M.J.C.: Representing a logic in the LCF metalanguage. In: N\u00e9el, D. (ed.) Tools and notions for program construction: an advanced course, pp. 163\u2013185. Cambridge University Press, Cambridge (1982)"},{"key":"8_CR21","volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M.J.C. Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/BFb0097791","volume-title":"Types for Proofs and Programs","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Proof style. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, pp. 154\u2013172. Springer, Heidelberg (1998)"},{"key":"8_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1591-5","volume-title":"Theorem Proving with the Real Numbers","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998) Revised version of author\u2019s PhD thesis"},{"key":"8_CR26","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.V. Harrison","year":"1999","unstructured":"Harrison, J.V.: 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, pp. 113\u2013130. Springer, Heidelberg (1999)"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-40922-X_14","volume-title":"Formal Methods in Computer-Aided Design","author":"J.V. Harrison","year":"2000","unstructured":"Harrison, J.V.: Formal verification of floating point trigonometric functions. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 217\u2013233. Springer, Heidelberg (2000)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formal verification of IA-64 division algorithms. In: Aagaard, Harrison (eds.) [1], pp. 234\u2013251","DOI":"10.1007\/3-540-44659-1_15"},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1022973506233","volume":"22","author":"J. Harrison","year":"2003","unstructured":"Harrison, J.: Formal verification of square root algorithms. Formal Methods in System Design\u00a022, 143\u2013153 (2003)","journal-title":"Formal Methods in System Design"},{"key":"8_CR30","first-page":"148","volume-title":"Proceedings, 16th IEEE Symposium on Computer Arithmetic","author":"J. Harrison","year":"2003","unstructured":"Harrison, J.: Isolating critical cases for reciprocals using integer factorization. In: Bajard, J.-C., Schulte, M. (eds.) Proceedings, 16th IEEE Symposium on Computer Arithmetic, Santiago de Compostela, Spain, pp. 148\u2013157. IEEE Computer Society, Los Alamitos (2003), currently available from symposium Web site at: \n                  \n                    http:\/\/www.dec.usc.es\/arith16\/papers\/paper-150.pdf"},{"key":"8_CR31","unstructured":"Holm, J.E.: Floating-Point Arithmetic and Program Correctness Proofs. PhD thesis, Cornell University (1980)"},{"key":"8_CR32","unstructured":"IEEE. Standard for binary floating point arithmetic. ANSI\/IEEE Standard 754-1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York 10017, USA (1985)"},{"key":"8_CR33","unstructured":"Jacobi, C.: Formal Verification of a Fully IEEE Compliant Floating Point Unit. PhD thesis, University of the Saarland (2002), available on the Web as: \n                  \n                    http:\/\/engr.smu.edu\/~seidel\/research\/diss-jacobi.ps.gz"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Kaivola, R., Aagaard, M.D.: Divider circuit verification with model checking and theorem proving. In: Aagaard, Harrison (eds.) [1], pp. 338\u2013355","DOI":"10.1007\/3-540-44659-1_21"},{"key":"8_CR35","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01932946","volume":"14","author":"S. Linnainmaa","year":"1974","unstructured":"Linnainmaa, S.: Analysis of some known methods of improving the accuracy of floating-point sums. BIT\u00a014, 167\u2013202 (1974)","journal-title":"BIT"},{"key":"8_CR36","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"Loveland, D.W.: Mechanical theorem-proving by model elimination. Journal of the ACM\u00a015, 236\u2013251 (1968)","journal-title":"Journal of the ACM"},{"key":"8_CR37","volume-title":"IA-64 and Elementary Functions: Speed and Precision","author":"P. Markstein","year":"2000","unstructured":"Markstein, P.: IA-64 and Elementary Functions: Speed and Precision. Prentice-Hall, Englewood Cliffs (2000)"},{"key":"8_CR38","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1147\/rd.341.0111","volume":"34","author":"P.W. Markstein","year":"1990","unstructured":"Markstein, P.W.: Computation of elementary functions on the IBM RISC System\/6000 processor. IBM Journal of Research and Development\u00a034, 111\u2013119 (1990)","journal-title":"IBM Journal of Research and Development"},{"key":"8_CR39","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/BF01975722","volume":"5","author":"O. M\u00f8ller","year":"1965","unstructured":"M\u00f8ller, O.: Quasi double-precision in floating-point addition. BIT\u00a05, 37\u201350 (1965)","journal-title":"BIT"},{"key":"8_CR40","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the correctness of the kernel of the AMD5\n                  K\n                86 floating-point division program. IEEE Transactions on Computers\u00a047, 913\u2013926 (1998)","journal-title":"IEEE Transactions on Computers"},{"key":"8_CR41","first-page":"530","volume-title":"Proceedings of the 38th Design Automation Conference (DAC 2001)","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535. ACM Press, New York (2001)"},{"key":"8_CR42","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2646-6","volume-title":"Elementary functions: Algorithms and Implementation","author":"J.-M. Muller","year":"1997","unstructured":"Muller, J.-M.: Elementary functions: Algorithms and Implementation. Birkh\u00e4user, Basel (1997)"},{"key":"8_CR43","unstructured":"Muller, J.-M.: On the definition of ulp(x). Research Report 2005-09, ENS Lyon (2005)"},{"key":"8_CR44","first-page":"1","volume":"1999-Q1","author":"J. O\u2019Leary","year":"1999","unstructured":"O\u2019Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal\u00a01999-Q1, 1\u201314 (1999), available on the Web as: \n                  \n                    http:\/\/developer.intel.com\/technology\/itj\/q11999\/articles\/art\/_5.htm","journal-title":"Intel Technology Journal"},{"key":"8_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-59293-8_189","volume-title":"TAPSOFT \u201995: Theory and Practice of Software Development","author":"V.R. Pratt","year":"1995","unstructured":"Pratt, V.R.: Anatomy of the Pentium bug. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol.\u00a0915, pp. 97\u2013107. Springer, Heidelberg (1995)"},{"key":"8_CR46","unstructured":"Priest, D.M.: On Properties of Floating Point Arithmetics: Numerical Stability and the Cost of Accurate Computations. PhD thesis, University of California, Berkeley (1992), available on the Web as: \n                  \n                    ftp:\/\/ftp.icsi.berkeley.edu\/pub\/theory\/priest-thesis.ps.Z"},{"key":"8_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent programs in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 195\u2013220. Springer, Heidelberg (1982)"},{"key":"8_CR48","unstructured":"Quinn, K.: Ever had problems rounding off figures? The stock exchange has. Wall Street Journal (November 8, 1983)"},{"key":"8_CR49","first-page":"337","volume":"199","author":"M.E. Remes","year":"1934","unstructured":"Remes, M.E.: Sur le calcul effectif des polynomes d\u2019approximation de Tchebichef. Comptes Rendus Hebdomadaires des S\u00e9ances de l\u2019Acad\u00e9mie des Sciences\u00a0199, 337\u2013340 (1934)","journal-title":"Comptes Rendus Hebdomadaires des S\u00e9ances de l\u2019Acad\u00e9mie des Sciences"},{"key":"8_CR50","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Rusinoff","year":"1998","unstructured":"Rusinoff, D.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998), available on the Web via: \n                  \n                    http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"8_CR51","unstructured":"Sawada, J.: Formal verification of divide and square root algorithms using series calculation. In: Borrione, D., Kaufmann, M., Moore, J. (eds.) 3rd International Workshop on the ACL2 Theorem Prover and its Applications, pp. 31\u201349. University of Grenoble (2002)"},{"key":"8_CR52","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design\u00a06, 147\u2013189 (1995)","journal-title":"Formal Methods in System Design"},{"key":"8_CR53","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/B978-0-08-040953-5.50011-8","volume-title":"Safety of Computer Control Systems, 1990 (SAFECOMP 1990)","author":"G. St\u00e5lmarck","year":"1990","unstructured":"St\u00e5lmarck, G., S\u00e4flund, M.: Modeling and verifying systems and software in propositional logic. In: Daniels, B.K. (ed.) Safety of Computer Control Systems, 1990 (SAFECOMP 1990), Gatwick, UK, pp. 31\u201336. Pergamon Press, Oxford (1990)"},{"key":"8_CR54","volume-title":"Floating-Point Computation","author":"P.H. Sterbenz","year":"1974","unstructured":"Sterbenz, P.H.: Floating-Point Computation. Prentice-Hall, Englewood Cliffs (1974)"},{"key":"8_CR55","first-page":"4","volume-title":"Proceedings, 14th IEEE symposium on on computer arithmetic","author":"S. Story","year":"1999","unstructured":"Story, S., Tang, P.T.P.: New algorithms for improved transcendental functions on IA-64. In: Koren, I., Kornerup, P. (eds.) Proceedings, 14th IEEE symposium on on computer arithmetic, Adelaide, Australia, pp. 4\u201311. IEEE Computer Society, Los Alamitos (1999)"},{"key":"8_CR56","doi-asserted-by":"crossref","unstructured":"Tang, P.T.P.: Table-lookup algorithms for elementary functions and their error analysis. In: Kornerup, P., Matula, D.W. (eds.) Proceedings of the 10\n                  th\n                 Symposium on Computer Arithemtic, pp. 232\u2013236 (1991)","DOI":"10.1109\/ARITH.1991.145565"},{"key":"8_CR57","unstructured":"Weis, P., Leroy, X.: Le langage Caml. InterEditions (1993), see also the CAML Web page: \n                  \n                    http:\/\/pauillac.inria.fr\/caml\/"},{"key":"8_CR58","first-page":"68","volume":"6","author":"A.v. Wijngaarden","year":"1966","unstructured":"Wijngaarden, A.v.: Numerical analysis as an independent science. BIT\u00a06, 68\u201381 (1966)","journal-title":"BIT"},{"key":"8_CR59","series-title":"National Physical Laboratory Notes on Applied Science","volume-title":"Rounding Errors in Algebraic Processes","author":"J.H. Wilkinson","year":"1963","unstructured":"Wilkinson, J.H.: Rounding Errors in Algebraic Processes. National Physical Laboratory Notes on Applied Science, vol.\u00a032. Her Majesty\u2019s Stationery Office (HMSO), London (1963)"},{"key":"8_CR60","volume-title":"Systematic Programming: An Introduction","author":"N. Wirth","year":"1973","unstructured":"Wirth, N.: Systematic Programming: An Introduction. Prentice-Hall, Englewood Cliffs (1973)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Hardware Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11757283_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,12]],"date-time":"2019-03-12T03:20:41Z","timestamp":1552360841000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11757283_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540343042","9783540343059"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/11757283_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}