{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:44:18Z","timestamp":1725486258775},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433811"},{"type":"electronic","value":"9783540459880"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45988-x_16","type":"book-chapter","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T22:19:02Z","timestamp":1181168342000},"page":"193-206","source":"Crossref","is-referenced-by-count":1,"title":["PROSPER An Investigation into Software Architecture for Embedded Proof Engines"],"prefix":"10.1007","author":[{"given":"Thomas F.","family":"Melham","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"16_CR1","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, \u2018Combining theorem proving and trajectory evaluation in an industrial environment,\u2019 in ACM\/IEEE Design Automation Conference, Proceedings (1998), pp. 538\u2013541."},{"key":"16_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-48256-3_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. D. Aagaard","year":"1999","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, \u2018Lifted-.: A pragmatic implementation of combined model checking and theorem proving\u2019, in Theorem Proving in Higher Order Logics, edited by Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry, Lecture Notes in Computer Science, vol. 1690 (Springer-Verlag, 1999), pp. 23\u2013340."},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996","author":"S. Agerholm","year":"1999","unstructured":"S. Agerholm, \u2018Translating Specifications in VDM-SL to PVS\u2019, in Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996: Turku, August 1996: Proceedings, edited by J. von Wright, J. Grundy, and J. Harrison Lecture Notes in Computer Science, vol. 1690 (Springer-Verlag, 1999), pp. 1\u201316."},{"key":"16_CR4","unstructured":"S. Agerholm and H. Skj\u00f8dt, Automating a model checker for recursive modal assertions in HOL. Technical Report DAIMI IR-92, Computer Science Department (Aarhus University, 1990)."},{"key":"16_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-40006-0_3","volume-title":"Proceedings of the 8th European Workshop on Logics in AI (JELIA)","author":"W. Ahrendt","year":"2000","unstructured":"W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. H\u00e4hnle, W. Menzel, and P. H. Schmitt, \u2018The KeY approach: Integrating object oriented design and formal verification\u2019, in Proceedings of the 8th European Workshop on Logics in AI (JELIA), edited by M. Ojeda-Aciego, I. P. de Guzm\u00e1n, G. Brewka, and L. M. Pereira (eds.), Lecture Notes in Computer Science, vol. 1919 (Springer-Verlag, 2000), pp. 21\u201336"},{"key":"16_CR6","unstructured":"A. Armando, M. Kohlhase, and S. Ranise, \u2018Communication protocols for mathematical services based on KQML and OMRS\u2019, in Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium (Proceedings of the Eighth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), edited by M. Kerber and M. Kohlhase (A. K. Peters Ltd., 2001)."},{"key":"16_CR7","unstructured":"A. Armando and D. Zini, \u2018Interfacing computer algebra and deduction systems via the Logic Broker Architecture\u2019, in Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium (Proceedings of the Eighth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), edited by M. Kerber and M. Kohlhase (A. K. Peters Ltd., 2001)."},{"key":"16_CR8","unstructured":"A. Armando and D. Zini, \u2018Towards Interoperable Mechanized Reasoning Systems: the Logic Broker Architecture\u2019, in Proceedings of the AI * IA-TABOO Joint Workshop \u2018Dagli Oggetti agli Agenti: Tendenze Evolutive dei Sistemi Software\u2019, 29\u201330 May 2001, Parma, Italy (2001), pp. 70\u201375."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"F. Baader and K. U. Schulz, eds., Frontiers of Combining Systems: First InternationalWorkshop, Munich, March 1996, Applied Logic Series, vol. 3 (Kluwer Academic Publishers, 1996).","DOI":"10.1007\/978-94-009-0349-4"},{"key":"16_CR10","unstructured":"L. Bening and H. Foster, Principles of Verifiable RTL Design (Kluwer, 2000)."},{"key":"16_CR11","unstructured":"S. Bensalem, V. Ganesh, Y. Lakhnech, C. Mu\u00f1oz, S. Owre, H. Ruess, J. Rushby, V. Rusu, H. Sa\u00efdi, N. Shankar, E. Singerman, and A. Tiwari, \u2018An overview of SAL\u2019, in Proceedings of the Fifth NASA Langley Formal Methods Workshop, June 2000 (Williamsburg, 2000)."},{"key":"16_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/BFb0028771","volume-title":"Proceedings of the 10th InternationalConfer ence on Computer Aided Verification (CAV\u201998)","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre, \u2018InVeSt: A tool for the verification of invariants\u2019, in Proceedings of the 10th InternationalConfer ence on Computer Aided Verification (CAV\u201998), edited by A. J. Hu and M. Y. Vardi, Lecture Notes in Computer Science, vol. 1427 (Springer-Verlag, 1998), pp. 505\u2013510."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller and V. Sorge, \u2018\u03a9-Ants \u2014 An open approach at combining interactive and automated theorem proving\u2019 in Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium (Proceedings of the Eighth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), edited by M. Kerber and M. Kohlhase (A. K. Peters Ltd., 2001).","DOI":"10.1201\/9781439864234"},{"key":"16_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/3-540-46419-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000","author":"P. Braun","year":"2000","unstructured":"P. Braun, H. L\u00f6tzbeyer, B. Sch\u00e4tz, and O. Slotosch, \u2018Consistent integration of formal methods\u2019, in Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000: Berlin, March\/April2000: Proceedings, edited by S. Graf and M. Schwartzbach, Lecture Notes in Computer Science, vol. 1785 (Springer-Verlag, 2000), pp. 48\u201362."},{"key":"16_CR15","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church, \u2018A Formulation of the Simple Theory of Types\u2019, Journalof Symbolic Logic, vol. 5 (1940), pp. 56\u201368.","journal-title":"Journalof Symbolic Logic"},{"key":"16_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Proceedings of the Eleventh Conference on Computer-Aided Verification (CAV\u201999)","author":"A. Cimatti","year":"1999","unstructured":"A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri, \u2018NuSMV: a new Symbolic Model Verifier\u2019, in Proceedings of the Eleventh Conference on Computer-Aided Verification (CAV\u201999), edited by N. Halbwachs and D. Peled, Lecture Notes in Computer Science, vol. 1633 (Springer-Verlag, 1999), pp. 495\u2013499."},{"key":"16_CR17","unstructured":"A. Coglio, \u2018The control component of OMRS: NQTHM as a case study\u2019, in Proceedings of the First Workshop on Abstraction, Analogy and Metareasoning, IRST (Trento, 1996), pp. 65\u201371."},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"G. Collins and L. A. Dennis, \u2018System description: Embedding verification into Microsoft Excel\u2019, in Proceedings of the 17th International Conference on Automated Deduction: CADE-17, edited by D. McAllester, Lecture Notes in Artificial Intelligence, vol. 1831 (Springer-Verlag, 2000), pp. 497\u2013501.","DOI":"10.1007\/10721959_40"},{"key":"16_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/3-540-44659-1_7","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000","author":"B. Colwell","year":"2000","unstructured":"B. Colwell and B. Brennan, \u2018Intel\u2019s Formal Verification Experience on the Willamette Development\u2019, in Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000: Portland, August2000: Proceedings, edited by M. Aagaard and J. Harrision, Lecture Notes in Computer Science, vol. 1869 (Springer-Verlag, 2000), pp. 106\u2013107."},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"B. I. Dahn, J. Gehne, T. Honigmann, and A. Wolf, \u2018Integration of automated and interactive theorem proving in ILF\u2019, in Proceedings of the 14th International Conference on Automated Deduction (CADE-14), edited by W. McCune, Lecture Notes in Artificial Intelligence, vol. 1249 (Springer-Verlag, 1997), pp. 57\u201360.","DOI":"10.1007\/3-540-63104-6_7"},{"key":"16_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-46419-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000","author":"L. A. Dennis","year":"2000","unstructured":"L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham, \u2018The Prosper Toolkit\u2019, in Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000: Berlin, March\/April 2000: Proceedings, edited by S. Graf and M. Schwartzbach, Lecture Notes in Computer Science, vol. 1785 (Springer-Verlag, 2000), pp. 78\u201392. An extended version of this paper is to appear in the InternationalJournalon Software Tools for Technology Transfer."},{"key":"16_CR22","unstructured":"L. Dennis, G. Collins, R. Boulton, G. Robinson, M. Norrish, and K. Slind, The PROSPER Toolkit, version 1.4, Part of deliverable D3.5, ESPRIT LTR Project Prosper (26241), Department of Computing Science, University of Glasgow (April, 2001). Available as prosper1-4.ps.gz at http:\/\/www.dcs.gla.ac.uk\/prosper\/toolkit\/ ."},{"key":"16_CR23","unstructured":"D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe, Extended static checking, Research Report 159, Compaq Systems Research Center, Palo Alto (December, 1998)."},{"key":"16_CR24","unstructured":"J. Fitzgerald and P. G. Larsen, Modelling Systems: Practical Tools and Techniques in Software Development (Cambridge University Press, 1998)."},{"key":"16_CR25","first-page":"156","volume":"5","author":"A. Franke","year":"1999","unstructured":"A. Franke, S. M. Hess, C. G. Jung, M. Kohlhase, and V. Sorge, \u2018Agent-Oriented Integration of Distributed Mathematical Services\u2019, Journalof UniversalComputer Science, vol. 5 (1999), pp. 156\u2013187.","journal-title":"Journalof UniversalComputer Science"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"A. Franke and M. Kohlhase, \u2018System description: MBase, an open mathematical knowledge base\u2019, in Proceedings of the 17th InternationalConfer ence on Automated Deduction: CADE-17, edited by D. McAllester, Lecture Notes in Artificial Intelligence, vol. 1831 (Springer-Verlag, 2000), pp. 455\u2013459.","DOI":"10.1007\/10721959_36"},{"key":"16_CR27","unstructured":"D. Fuchs and J. Denzinger, Knowledge-based cooperation between theorem provers by TECHS, SEKI-Report SR-97-11 (University of Kaiserslautern, 1997)."},{"key":"16_CR28","unstructured":"D. M. Gabbay and M. de Rijke, eds., Frontiers of Combining Systems 2, Studies in Logic and Computation Series (Research Studies Press, 2000)."},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia, P. Pecchiari, and C. Talcott, \u2018Reasoning theories: Towards an architecture for open mechanized reasoning systems\u2019, in Frontiers of Combining Systems: First International Workshop, Munich, March 1996, edited by F. Baader and K. U. Schulz, Applied Logic Series, vol. 3 (Kluwer Academic Publishers, 1996), pp. 157\u2013174.","DOI":"10.1007\/978-94-009-0349-4_8"},{"key":"16_CR30","unstructured":"M. Gordon and K. F. Larsen, Combining the Hol98 proof assistant with the BuDDy BDD package, Technical Report 481, University of Cambridge Computer Laboratory (December, 1999)."},{"key":"16_CR31","unstructured":"M. J. C. Gordon and T. F. Melham, eds., Introduction to HOL: A theorem proving environment for higher order logic (Cambridge University Press, 1993)."},{"key":"16_CR32","first-page":"275","volume":"1","author":"A. Holt","year":"2000","unstructured":"A. Holt, E. Klein, and C. Grover, \u2018Natural language specifications for hardware verification\u2019, Language and Computation, vol. 1 (2000), pp. 275\u2013282. Special issue on ICoS-1.","journal-title":"Language and Computation"},{"key":"16_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-48153-2_13","volume-title":"Correct Hardware Design and Verification Methods: 10th IFIP WG10.5 Advanced Research Working Conference: Bad Herrenalb","author":"D. W. Hoffmann","year":"1999","unstructured":"D. W. Hoffmann and T. Kropf, \u2018Automatic error correction of large circuits using boolean decomposition and abstraction\u2019, in Correct Hardware Design and Verification Methods: 10th IFIP WG10.5 Advanced Research Working Conference: Bad Herrenalb, September 1999: Proceedings, edited by L. Pierre and T. Kropf, Lecture Notes in Computer Science, vol. 1703 (Springer-Verlag, 1999), pp. 157\u2013171."},{"key":"16_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"J. Hurd, \u2018Integrating Gandalf and HOL\u2019, in Theorem Proving in Higher Order Logics, edited by Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry, Lecture Notes in Computer Science, vol. 1690 (Springer-Verlag, 1999), pp. 311\u2013321."},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"M. Kaufmann, P. Manolios, and J S. Moore, Computer-Aided Reasoning: An Approach (Kluwer Academic Publishers, 2000).","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"H. Kirchner and C. Ringeissen, eds., Frontiers of Combining Systems: Third InternationalWorkshop, FroCoS 2000: Nancy, March 2000: Proceedings, Lecture Notes in Artificial Intelligence, vol. 1794 (Springer-Verlag, 2000).","DOI":"10.1007\/10720084"},{"key":"16_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1186","DOI":"10.1007\/3-540-48118-4_13","volume-title":"FM\u201999-Formal Methods","author":"B. Krieg-Br\u00fcckner","year":"1999","unstructured":"B. Krieg-Br\u00fcckner, J. Peleska, E.-R. Olderog, and A. Baer, \u2018The UniForM Work-Bench, a universal development environment for formal methods\u2019, in FM\u201999-Formal Methods, edited by J. M. Wing, J. Woodcock, and J. Davies, vol. 2, Lecture Notes in Computer Science, vol. 1709 (Springer-Verlag, 1999), pp. 1186\u20131205."},{"key":"16_CR38","doi-asserted-by":"crossref","unstructured":"K. L. McMillan, Symbolic Model Checking (Kluwer Academic Publishers, 1993).","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"16_CR39","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K. L. McMillan","year":"1999","unstructured":"K. L. McMillan, \u2018Verification of infinite state systems by compositional model checking\u2019, in Correct Hardware Design and Verification Methods, edited by L. Pierre and T. Kropf, Lecture Notes in Computer Science, vol. 1703 (Springer-Verlag, 1999), pp. 219\u2013233."},{"key":"16_CR40","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference, CHARME 2001","author":"K. L. McMillan","year":"2001","unstructured":"K. L. McMillan, \u2018Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking\u2019, in Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference, CHARME 2001: Livingston, Scotland, UK, September 4\u20137 2001: Proceedings, edited by T. Margaria and T. Melham, Lecture Notes in Computer Science, vol. 2144, (Springer-Verlag, 2001), pp. 179\u2013195."},{"key":"16_CR41","unstructured":"Microsoft Corporation, Microsoft Excel, http:\/\/www.microsoft.com\/excel ."},{"key":"16_CR42","doi-asserted-by":"crossref","unstructured":"R. Milner, M. Tofte, R. Harper, and D. MacQueen, The Definition of Standard ML, revised edition (MIT Press, 1997).","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"16_CR43","unstructured":"N. Mokhoff, \u2018Intel, Motorola report formal verification gains\u2019, The EE Times Online, http:\/\/www.eetimes.com\/story\/OEG20010621S0080 ."},{"key":"16_CR44","unstructured":"Object Management Group, The Common Object Request Broker: Architecture and Specification, OMG Technical Report (July 1995)."},{"key":"16_CR45","unstructured":"J. O'Leary, X. Zhao, R. Gerth, and C.-J. H. Seger, \u2018Formally verifying IEEE compliance of floating-point hardware\u2019, Intel Technology Journal (First Quarter, 1999). Available online at http:\/\/developer.intel.com\/technology\/itj\/ ."},{"key":"16_CR46","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Proceedings of the International Conference on Computer-Aided Verification","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M. Srivas, \u2018An integration of model checking and automated proof checking\u2019, in Proceedings of the International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, vol. 939 (Springer-Verlag, 1995), pp. 84\u201397."},{"key":"16_CR47","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/3-540-48256-3_17","volume-title":"A HOL Conversion for Translating Linear Time Temporal Logic to \u03c9-Automata","author":"K. Schneider","year":"1999","unstructured":"K. Schneider and D. W. Hoffmann, \u2018A HOL Conversion for Translating Linear Time Temporal Logic to \u03c9-Automata\u2019, in Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, Nice, 14\u201317 September, 1999, Lecture Notes in Computer Science, vol. 1690 (Springer-Verlag, 1999), pp. 255\u2013"},{"key":"16_CR48","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J. H. Seger","year":"1995","unstructured":"C.-J. H. Seger and R. E. Bryant, \u2018Formal verification by symbolic evaluation of partially-ordered trajectories\u2019, Formal Methods in System Design, vol. 6 (1995), pp. 147\u2013189.","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"16_CR49","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M. Sheeran","year":"2000","unstructured":"M. Sheeran and G. St\u00e5lmarck, \u2018A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic\u2019, Formal Methods in System Design, vol. 16, no. 1 (2000), pp. 23\u201358.","journal-title":"Formal Methods in System Design"},{"key":"16_CR50","unstructured":"M. Staples, Linking ACL2 and HOL, Technical Report 476, University of Cambridge Computer Laboratory (1999)."},{"key":"16_CR51","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s100090050003","volume":"1","author":"B. Steffen","year":"1997","unstructured":"B. Steffen, T. Margaria, and V. Braun, \u2018The Electronic Tool Integration Platform: concepts and design\u2019, International Journalon Software Tools for Technology Transfer, vol. 1 (1997), pp. 9\u201330.","journal-title":"International Journalon Software Tools for Technology Transfer"},{"key":"16_CR52","unstructured":"A. Stevenson and L. A. Dennis, \u2018Integrating SVC and HOL with the Prosper Toolkit\u2019, in Supplemental Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2000), OGI Technical Report CSE 00-009, Oregon Graduate Institute (August, 2000), pp. 199\u2013206."},{"key":"16_CR53","unstructured":"T. E. Uribe, \u2018Combinations of Model Checking and Theorem Proving\u2019, in Frontiers of Combining Systems: Third InternationalWorkshop, FroCoS 2000: Nancy, March 2000: Proceedings, edited by H. Kirchner and C. Ringeissen, Lecture Notes in Artificial Intelligence, vol. 1794 (Springer-Verlag, 2000), pp. 151\u2013170."}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45988-X_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:44:03Z","timestamp":1556466243000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45988-X_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433811","9783540459880"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/3-540-45988-x_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}