{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:52:07Z","timestamp":1725558727618},"publisher-location":"Berlin, Heidelberg","reference-count":61,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540205272"},{"type":"electronic","value":"9783540400073"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-40007-3_23","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T20:04:10Z","timestamp":1277496250000},"page":"367-380","source":"Crossref","is-referenced-by-count":1,"title":["Verification by Abstraction"],"prefix":"10.1007","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"23_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Information and Computation\u00a0104(1), 2\u201334 (1993)","journal-title":"Information and Computation"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Reachability analysis of hybrid systems via predicate abstraction. In: Tomlin and Greenstreet [TG02], pp. 35\u201348","DOI":"10.1007\/3-540-45873-5_6"},{"key":"23_CR3","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":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-46419-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Baukus","year":"2000","unstructured":"Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting WS1S systems to verify parameterized networks. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 188\u2013203. Springer, Heidelberg (2000)"},{"issue":"1","key":"23_CR5","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N. Bjorner","year":"1997","unstructured":"Bjorner, N., Browne, I.A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoretical Computer Science\u00a0173(1), 49\u201387 (1997)","journal-title":"Theoretical Computer Science"},{"key":"23_CR6","unstructured":"Bensalem, S., Ganesh, V., Lakhnech, Y., Mu\u00f1oz, C., Owre, S., Rue\u00df, H., Rushby, J., Rusu, V., Sa\u00efdi, H., Shankar, N., Singerman, E., Tiwari, A.: An overview of SAL. In: Holloway, C.M. (ed.) LFM 2000: Fifth NASA Langley Formal Methods Workshop, Hampton, VA, pp. 187\u2013196 (2000), NASA Langley Research Center. Proceedings available at http:\/\/shemesh.larc.nasa.gov\/fm\/Lfm2000\/Proc\/"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Hu and Vardi [HV98], pp. 319\u2013331","DOI":"10.1007\/BFb0028755"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Lakhnech, Y., Sa\u00efdi, H.: Powerful techniques for the automatic generation of invariants. In: Alur, Henzinger [AH96], pp. 323\u2013335","DOI":"10.1007\/3-540-61474-5_80"},{"key":"23_CR9","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/378795.378846","volume-title":"Proceedings of the SIGPLAN 2001 Conference on Programming Language Design and Implementation, 2001","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Proceedings of the SIGPLAN 2001 Conference on Programming Language Design and Implementation, 2001, pp. 203\u2013313. ACM Press, New York (2001)"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis. In: 4th ACM Symposium on Principles of Programming Languages. Association for Computing Machinery (January 1977)","DOI":"10.1145\/512950.512973"},{"issue":"2-3","key":"23_CR11","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming\u00a013(2-3), 103\u2013179 (1992)","journal-title":"Journal of Logic Programming"},{"key":"23_CR12","first-page":"439","volume-title":"22nd International Conference on Software Engineering","author":"J. Corbett","year":"2000","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, J., Laubach, S., Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: 22nd International Conference on Software Engineering, Limerick, Ireland, pp. 439\u2013448. IEEE Computer Society, Los Alamitos (2000)"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: Nineteenth Annual ACM Symposium on Principles of Programming Languages, pp. 343\u2013354 (1992)","DOI":"10.1145\/143165.143235"},{"key":"23_CR15","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":"23_CR16","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables. In: 5th ACM Symposium on Principles of Programming Languages. Association for Computing Machinery (January 1978)","DOI":"10.1145\/512760.512770"},{"issue":"3","key":"23_CR17","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G.E. Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition. Journal of Symbolic Computation\u00a012(3), 299\u2013328 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M.A., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Hu, Vardi [HV98], pp. 293\u2013304","DOI":"10.1007\/BFb0028753"},{"key":"23_CR19","unstructured":"Dams, D.R.: Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands (July 1996)"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: Annual IEEE Symposium on Logic in Computer Science 2001, pp. 51\u201360. The Institute of Electrical and Electronics Engineers (2001)","DOI":"10.1109\/LICS.2001.932482"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs and Peled [HP99], pp. 160\u2013171","DOI":"10.1007\/3-540-48683-6_16"},{"key":"23_CR22","unstructured":"Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems: Abstractions preserving \u2200CTL*, \u2203CTL* and CTL*. In: Olderog, E.-R. (ed.) Programming Concepts, Methods and Calculi (PROCOMET 1994), pp. 561\u2013581 (1994)"},{"key":"23_CR23","unstructured":"Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. Technical Report 159, COMPAQ Systems Research Center (1998)"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: ACM Symposium on Principles of Programming Languages 2002. Association for Computing Machinery, pp. 191\u2013202 (January 2002)","DOI":"10.1145\/503272.503291"},{"key":"23_CR25","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":"23_CR26","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Verifying invariants using theorem proving. In: Alur, R., Henzinger, T.A. (eds.) [AH96], pp. 196\u2013207","DOI":"10.1007\/3-540-61474-5_69"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: ACM Symposium on Principles of Programming Languages 2002. Association for Computing Machinery, pp. 58\u201370 (January 2002)","DOI":"10.1145\/503272.503279"},{"issue":"11","key":"23_CR28","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C. Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Kirby Jr., J., Labaw, B., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering\u00a024(11), 927\u2013948 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"10","key":"23_CR29","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM\u00a012(10), 576\u2013583 (1969)","journal-title":"Comm. ACM"},{"key":"23_CR30","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, Englewood Cliffs (1991)"},{"key":"23_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"1999","unstructured":"Halbwachs, N., Peled, D.A. (eds.): CAV 1999. LNCS, vol.\u00a01633. Springer, Heidelberg (1999)"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"1998","unstructured":"Hu, A.J., Vardi, M.Y. (eds.): CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. In: Sixth ACM SIGSOFT Symposium on the Foundations of Software Engineering, Lake Buena Vista, FL. Association for Computing Machinery, pp. 56\u201369 (November 1998)","DOI":"10.1145\/288195.288218"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. In: Eighth ACM Symposium on Principles of Distributed Computing, Edmonton, Alberta, Canada, August 1989, pp. 239\u2013248 (1989)","DOI":"10.1145\/72981.72998"},{"key":"23_CR35","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)"},{"issue":"1","key":"23_CR36","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation\u00a0163(1), 203\u2013243 (2000)","journal-title":"Information and Computation"},{"key":"23_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-48168-0_11","volume-title":"Computer Science Logic","author":"Y. Kesten","year":"1999","unstructured":"Kesten, Y., Pnueli, A., Vardi, M.Y.: Verification by augmented abstraction: The automata-theoretic view. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 141\u2013156. Springer, Heidelberg (1999)"},{"key":"23_CR38","volume-title":"Automata-Theoretic Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1993","unstructured":"Kurshan, R.P.: Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, Princeton (1993)"},{"key":"23_CR39","doi-asserted-by":"publisher","first-page":"11","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, 11\u201344 (1995)","journal-title":"Formal Methods in System Design"},{"key":"23_CR40","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"2nd International Workshop on Verification of Infinite State Systems: Infinity 1997","author":"D. Lesens","year":"1997","unstructured":"Lesens, D., Sa\u00efdi, H.: Automatic verification of parameterized networks of processes by abstraction. In: Moller, F. (ed.) 2nd International Workshop on Verification of Infinite State Systems: Infinity 1997, Bologna, Italy. Electronic Notes in Theoretical Computer Science, vol.\u00a09. Elsevier, Amsterdam (1997)"},{"key":"23_CR41","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)"},{"key":"23_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-49519-3_1","volume-title":"Formal Methods in Computer-Aided Design","author":"K. McMillan","year":"1998","unstructured":"McMillan, K.: Minimalist proof assistants: Interactions of technology and methodology in formal system level verification. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 1\u20131. Springer, Heidelberg (1998), Invited presentation\u2014no paper in proceedings, but slides available at http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/"},{"key":"23_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/3-540-63875-X_41","volume-title":"Advances in Computing Science - ASIAN\u201997","author":"S. Merz","year":"1997","unstructured":"Merz, S.: Rules for abstraction. In: Shyamasundar, R.K. (ed.) ASIAN 1997. LNCS, vol.\u00a01345, pp. 32\u201345. Springer, Heidelberg (1997)"},{"key":"#cr-split#-23_CR44.1","doi-asserted-by":"crossref","unstructured":"M\u00f6ller, M.O., Rue\u00df, H., Sorea, M.: Predicate abstraction for dense real-time systems. Electronic Notes in Theoretical Computer Science\u00a065(6) (2002);","DOI":"10.7146\/brics.v8i44.21704"},{"key":"#cr-split#-23_CR44.2","unstructured":"Full version available as Technical Report BRICS-RS- 01-44, Department of Computer Science, University of Aarhus, Denmark"},{"key":"23_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/10722167_33","volume-title":"Computer Aided Verification","author":"K. Namjoshi","year":"2000","unstructured":"Namjoshi, K., Kurshan, R.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 435\u2013449. Springer, Heidelberg (2000)"},{"issue":"8","key":"23_CR46","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1109\/71.406955","volume":"6","author":"F. Pong","year":"1995","unstructured":"Pong, F., Dubois, M.: A new approach for the verification of cache coherence protocols. IEEE Transactions on Parallel and Distributed Systems\u00a06(8), 773\u2013787 (1995)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"23_CR47","doi-asserted-by":"crossref","unstructured":"Pardo, A., Hachtel, G.D.: Automatic abstraction techniques for propositional mu-calculus model checking. In: Grumberg [Gru97], pp. 12\u201323","DOI":"10.1007\/3-540-63166-6_5"},{"key":"23_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1,\u2009\u221e\u2009)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 107. Springer, Heidelberg (2002)"},{"key":"23_CR49","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, pp. 178\u2013192. Springer, Heidelberg (1999)"},{"key":"23_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-540-45099-3_20","volume-title":"Static Analysis","author":"H. Sa\u00efdi","year":"2000","unstructured":"Sa\u00efdi, H.: Model checking guided abstraction and analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 377\u2013396. Springer, Heidelberg (2000)"},{"key":"23_CR51","unstructured":"Sa\u00efdi, H., Graf, S.: Construction of abstract state graphs with PVS. In: Grumberg [Gru97], pp. 72\u201383"},{"key":"23_CR52","volume-title":"Essays on Programming Methodology","author":"N. Shankar","year":"2002","unstructured":"Shankar, N.: Automated verification using deduction, exploration, and abstraction. In: Essays on Programming Methodology. Springer, Heidelberg (2002)"},{"key":"23_CR53","doi-asserted-by":"crossref","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs and Peled [HP99], pp. 443\u2013454","DOI":"10.1007\/3-540-48683-6_38"},{"key":"23_CR54","doi-asserted-by":"crossref","unstructured":"Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. In: Alur and Henzinger [AH96], pp. 208\u2013219","DOI":"10.1007\/3-540-61474-5_70"},{"key":"23_CR55","series-title":"Lecture Notes in Computer Science","volume-title":"Hybrid Systems: Computation and Control","year":"2002","unstructured":"Tomlin, C.J., Greenstreet, M.R. (eds.): HSCC 2002. LNCS, vol.\u00a02289. Springer, Heidelberg (2002)"},{"key":"23_CR56","doi-asserted-by":"crossref","unstructured":"Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin and Greenstreet [TG02], pp. 465\u2013478","DOI":"10.1007\/3-540-45873-5_36"},{"key":"23_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-45319-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Tiwari","year":"2001","unstructured":"Tiwari, A., Rue\u00df, H., Sa\u00efdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 113\u2013127. Springer, Heidelberg (2001)"},{"key":"#cr-split#-23_CR58.1","unstructured":"Uribe, T.E.: Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Stanford University (1998);"},{"key":"#cr-split#-23_CR58.2","unstructured":"Available as Stanford University Computer Science Department Technical Report No. STAN-CS-TR-99-1618"},{"key":"23_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1990","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 68\u201380. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods at the Crossroads. From Panacea to Foundational Support"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40007-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T12:45:51Z","timestamp":1559220351000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40007-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540205272","9783540400073"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40007-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}