{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:47:03Z","timestamp":1725475623320},"publisher-location":"Berlin, Heidelberg","reference-count":58,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672814"},{"type":"electronic","value":"9783540464211"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10720084_11","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T09:36:30Z","timestamp":1167384990000},"page":"151-170","source":"Crossref","is-referenced-by-count":15,"title":["Combinations of Model Checking and Theorem Proving"],"prefix":"10.1007","author":[{"given":"Tom\u00e1s E.","family":"Uribe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"1996","unstructured":"Alur, R., Henzinger, T.A. (eds.): CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design","author":"C. Barrett","year":"1996","unstructured":"Barrett, C., Dill, D.L., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 187\u2013201. Springer, Heidelberg (1996)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Collaboration between Human and Artificial Societies","year":"1999","unstructured":"Padget, J. (ed.): Collaboration between Human and Artificial Societies 1997. LNCS, vol.\u00a01624. Springer, Heidelberg (1999)"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Design Autom. Conf., DAC 1999 (1999)","DOI":"10.21236\/ADA360973"},{"key":"11_CR6","unstructured":"Bj\u00f8rner, N.S.: Integrating Decision Procedures for Temporal Verification. PhD thesis, Comp. Sci. Department, Stanford Univ. (November 1998)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f3rner, N.S., Browne, A., Chang, E.S., Colon, M., Kapur, A., Manna, Z., Sipma, H.B., Uribe, T.E.: STeP: Deductive-algorithmic verification of reactive and real-time systems. In: [1], pp. 415\u2013418","DOI":"10.1007\/3-540-61474-5_92"},{"issue":"1","key":"11_CR8","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N.S. Bj\u00f8rner","year":"1997","unstructured":"Bj\u00f8rner, N.S., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoretical Comp. Sci.\u00a0173(1), 49\u201387 (1997)","journal-title":"Theoretical Comp. Sci."},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/3-540-63104-6_13","volume-title":"Automated Deduction - CADE-14","author":"N.S. Bj\u00f8rner","year":"1997","unstructured":"Bj\u00f8rner, N.S., Stickel, M.E., Uribe, T.E.: A practical integration of first-order reasoning and decision procedures. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 101\u2013115. Springer, Heidelberg (1997)"},{"issue":"1","key":"11_CR10","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(92)90183-G","volume":"96","author":"J.C. Bradfield","year":"1992","unstructured":"Bradfield, J.C., Stirling, C.: Local model checking for infinite state spaces. Theoretical Comp. Sci.\u00a096(1), 157\u2013174 (1992)","journal-title":"Theoretical Comp. Sci."},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/3-540-60692-0_69","volume-title":"15th Conf. on the Foundations of Software Technology and Theoretical Comp. Sci.","author":"A. Browne","year":"1995","unstructured":"Browne, A., Manna, Z., Sipma, H.B.: Generalized temporal verification diagrams. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 484\u2013498. Springer, Heidelberg (1995)"},{"issue":"8","key":"11_CR12","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(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using Presburger arithmetic. In: Grumberg [29], pp. 400\u2013411","DOI":"10.1007\/3-540-63166-6_39"},{"key":"11_CR14","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":"11_CR15","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Fujita, M., Zhao, X.: Hybrid decision diagrams. Overcoming the limitations of MTBDDs and BMDs. In: IEEE\/ACM Intl. Conf. on Computer-Aided Design, pp. 159\u2013163 (November 1995)","DOI":"10.21236\/ADA296684"},{"key":"11_CR16","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"C\u00f3lon, M.A., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 293\u2013304. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028753"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symp. Princ. of Prog. Lang, pp. 238\u2013252. ACM Press, New York (1977)","DOI":"10.1145\/512950.512973"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","first-page":"230","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W. Damm","year":"1995","unstructured":"Damm, W., Grumberg, O., Hungar, H.: What if model checking must be truly symbolic. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 230\u2013244. Springer, Heidelberg (1995)"},{"key":"11_CR20","unstructured":"Dams, D.R.: Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven Univ. of Technology (July 1996)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Manna, Z.: Temporal verification by diagram transformations. In: [1], pp. 287\u2013299","DOI":"10.1007\/3-540-61474-5_77"},{"key":"11_CR23","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Tech. Report 159, Compaq SRC (December 1998)"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: The Murp verification system. In: [1], pp. 390\u2013393","DOI":"10.1007\/3-540-61474-5_86"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-60045-0_40","volume-title":"Computer Aided Verification","author":"J. Dingel","year":"1995","unstructured":"Dingel, J., Filkorn, T.: Model checking of infinite-state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 54\u201369. Springer, Heidelberg (1995)"},{"key":"11_CR26","first-page":"70","volume-title":"Proc. 13th IEEE Symp. Logic in Comp. Sci.","author":"E.A. Emerson","year":"1998","unstructured":"Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: Proc. 13th IEEE Symp. Logic in Comp. Sci., pp. 70\u201380. IEEE Press, Los Alamitos (1998)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/3-540-49213-5_9","volume-title":"Compositionality: The Significant Difference","author":"B. Finkbeiner","year":"1998","unstructured":"Finkbeiner, B., Manna, Z., Sipma, H.B.: Deductive verification of modular systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 239\u2013275. Springer, Heidelberg (1998)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg [29], pp. 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"1997","unstructured":"Grumberg, O. (ed.): CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.: HYTECH: The Cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 265\u2013293. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60472-3_14"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/3-540-46541-3_2","volume-title":"STACS 2000","author":"T.A. Henzinger","year":"2000","unstructured":"Henzinger, T.A., Majumdar, R.: A classification of symbolic transition systems. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol.\u00a01770, p. 13. Springer, Heidelberg (2000)"},{"key":"11_CR32","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, Engelwood Cliffs (1991)"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/3-540-56922-7_13","volume-title":"Computer Aided Verification","author":"H. Hungar","year":"1993","unstructured":"Hungar, H.: Combining model checking and theorem proving to verify parallel processes. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 154\u2013165. Springer, Heidelberg (1993)"},{"key":"11_CR34","unstructured":"Jackson, D., Damon, C.A.: Nitpick reference manual. Tech. report, Carnegie-Mellon Univ. (1996)"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-49519-3_2","volume-title":"Formal Methods in Computer-Aided Design","author":"R.B. Jones","year":"1998","unstructured":"Jones, R.B., Skakkebask, J.U., Dill, D.L.: Reducing manual abstraction in formal verification of out-of-order execution. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 2\u201317. Springer, Heidelberg (1998)"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg [29], pp. 424\u2013435","DOI":"10.1016\/S0304-3975(00)00103-1"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/BFb0055757","volume-title":"Mathematical Foundations of Computer Science 1998","author":"Y. Kesten","year":"1998","unstructured":"Kesten, Y., Pnueli, A.: Modularization and abstraction: The keys to practical formal verification. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol.\u00a01450, pp. 54\u201371. Springer, Heidelberg (1998)"},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-56922-7_14","volume-title":"Computer Aided Verification","author":"R.P. Kurshan","year":"1993","unstructured":"Kurshan, R.P., Lamport, L.: Verification of a multiplier: 64 bits and beyond. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 166\u2013179. Springer, Heidelberg (1993)"},{"key":"11_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design\u00a06, 1\u201335 (1995)","journal-title":"Formal Methods in System Design"},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Lowry, M., Subramaniam, M.: Abstraction for analytic verification of concurrent software systems. In: Symp. on Abstraction, Reformulation, and Approx. (May 1998)","DOI":"10.1109\/5254.722359"},{"key":"11_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/3-540-49253-4_5","volume-title":"Algebraic Methodology and Software Technology","author":"Z. Manna","year":"1998","unstructured":"Manna, Z., Browne, A., Sipma, H.B., Uribe, T.E.: Visual abstractions for temporal verification. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol.\u00a01548, pp. 28\u201341. Springer, Heidelberg (1998)"},{"issue":"1","key":"11_CR42","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theoretical Comp. Sci.\u00a083(1), 97\u2013130 (1991)","journal-title":"Theoretical Comp. Sci."},{"key":"11_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"726","DOI":"10.1007\/3-540-57887-0_123","volume-title":"Theoretical Aspects of Computer Software","author":"Z. Manna","year":"1994","unstructured":"Manna, Z., Pnueli, A.: Temporal verification diagrams. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, pp. 726\u2013765. Springer, Heidelberg (1994)"},{"key":"11_CR44","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"11_CR45","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Pub., Dordrecht (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"11_CR46","doi-asserted-by":"crossref","unstructured":"M\u00fcller, O., Nipkow, T.: Combining model checking and deduction for I\/O-automata. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 1\u201312. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60630-0_1"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking and model checking. In: [1], pp. 411\u2013414.","DOI":"10.1007\/3-540-61474-5_91"},{"key":"11_CR48","first-page":"46","volume-title":"Proc. 18th IEEE Symp. Found. of Comp. Sci.","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. Found. of Comp. Sci., pp. 46\u201357. IEEE Computer Society Press, Los Alamitos (1977)"},{"key":"11_CR49","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: [1], pp. 184\u2013195","DOI":"10.1007\/3-540-61474-5_68"},{"key":"11_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J. Queille","year":"1982","unstructured":"Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"11_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer Aided Verification","author":"S. Rajan","year":"1995","unstructured":"Rajan, S., Shankar, N., Srivas, M.K.: An integration of model checking with automated proof checking. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 84\u201397. Springer, Heidelberg (1995)"},{"key":"11_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48234-2_1","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"J. Rushby","year":"1999","unstructured":"Rushby, J.: Integrated formal verification: Using model checking with automated abstraction, invariant generation, and theorem proving. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 1\u201311. Springer, Heidelberg (1999)"},{"key":"11_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-49059-0_13","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"V. Rusu","year":"1999","unstructured":"Rusu, V., Singerman, E.: On proving safety properties by integrating static analysis, theorem proving and abstraction. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 178. Springer, Heidelberg (1999)"},{"key":"11_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Saidi","year":"1999","unstructured":"Saidi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"11_CR55","doi-asserted-by":"crossref","unstructured":"Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Proc. 5th Static Analysis Symp. LNCS. Springer, Heidelberg (1998)","DOI":"10.1007\/3-540-49727-7_22"},{"key":"11_CR56","unstructured":"Sipma, H.B.: Diagram-based Verification of Discrete, Real-time and Hybrid Systems. PhD thesis, Comp. Sci. Department, Stanford Univ. (February 1999)"},{"issue":"1","key":"11_CR57","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1023\/A:1008791913551","volume":"15","author":"H.B. Sipma","year":"1999","unstructured":"Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. Formal Methods in System Design\u00a015(1), 49\u201374 (1999)","journal-title":"Formal Methods in System Design"},{"key":"11_CR58","unstructured":"Uribe, T.E.: Abstraction-based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Comp. Sci. Department, Stanford Univ., Tech. Report STAN-CS-TR-99-1618 (December 1998)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10720084_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T03:05:55Z","timestamp":1683687955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10720084_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672814","9783540464211"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/10720084_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}