{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:46:23Z","timestamp":1762458383297},"reference-count":72,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2005,2,1]],"date-time":"2005-02-01T00:00:00Z","timestamp":1107216000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2005,2]]},"DOI":"10.1007\/s10270-004-0058-x","type":"journal-article","created":{"date-parts":[[2004,3,31]],"date-time":"2004-03-31T16:15:42Z","timestamp":1080749742000},"page":"32-54","source":"Crossref","is-referenced-by-count":144,"title":["The KeY tool"],"prefix":"10.1007","volume":"4","author":[{"given":"Wolfgang","family":"Ahrendt","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Baar","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Beckert","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Giese","sequence":"additional","affiliation":[]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[]},{"given":"Wolfram","family":"Menzel","sequence":"additional","affiliation":[]},{"given":"Wojciech","family":"Mostowski","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Roth","sequence":"additional","affiliation":[]},{"given":"Steffen","family":"Schlager","sequence":"additional","affiliation":[]},{"given":"Peter H.","family":"Schmitt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,2,1]]},"reference":[{"key":"58_CR1","doi-asserted-by":"crossref","unstructured":"Ahrendt W (2002) Deductive search for errors in free data type specifications using model generation. In: Voronkov A (ed) Automated Deduction \u2013 CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, LNCS, vol 2392. Springer-Verlag","DOI":"10.1007\/3-540-45620-1_18"},{"key":"58_CR2","doi-asserted-by":"crossref","unstructured":"Ahrendt W, Baar T, Beckert B, Giese M, Habermalz E, H\u00e4hnle R, Menzel W, Schmitt PH (2000) The KeY approach: Integrating object oriented design and formal verification. In: Ojeda-Aciego M, de Guzm\u00e1n IP, Brewka G, Pereira LM (eds) Proc. 8th European Workshop on Logics in AI (JELIA), LNCS, vol 1919. Springer-Verlag, pp 21\u201336, Oct.","DOI":"10.1007\/3-540-40006-0_3"},{"key":"58_CR3","doi-asserted-by":"crossref","unstructured":"Ahrendt W, Baar T, Beckert B, Giese M, H\u00e4hnle R, Menzel W, Mostowski W, Schmitt PH (2002) The KeY system: Integrating object-oriented design and formal methods. In: Kutsche R-D, Weber H (eds) Fundamental Approaches to Software Engineering (FASE), Part of Joint European Conferences on Theory and Practice of Software, ETAPS, Grenoble, LNCS, vol 2306. Springer-Verlag, pp 327\u2013330","DOI":"10.1007\/3-540-45923-5_23"},{"key":"58_CR4","unstructured":"Androutsopoulos K (2002) Using SMV to model check RSDS specifications. Technical Report TR-02-07, King\u2019s College of London, Department of Computing Science"},{"key":"58_CR5","unstructured":"ANTLR homepage. At http:\/\/www.antlr.org\/"},{"key":"58_CR6","unstructured":"Baar T (2002) How to ground meta-circular OCL descriptions: A set-theoretic approach. In: Clark T, Evans A, Lano K (eds) Proceedings, Fourth Workshop on Rigorous Object-Oriented Methods, London"},{"key":"58_CR7","doi-asserted-by":"crossref","unstructured":"Baar T (2003) The definition of transitive closure with ocl: Limitations and applications. In: Proceedings, Fifth Andrei Ershov International Conference, Perspectives of System Informatics, Novosibirsk, Russia, LNCS, vol 2890. Springer, pp 358\u2013365, July","DOI":"10.1007\/978-3-540-39866-0_36"},{"key":"58_CR8","unstructured":"Baar T (2003) \u00dcber die Semantikbeschreibung OCL-artiger Sprachen. PhD thesis, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe. ISBN 3-8325-0433-8, Logos Verlag, Berlin"},{"key":"58_CR9","doi-asserted-by":"crossref","unstructured":"Baar T (2004) Metamodels without metacircularities. L\u2019Objet. To appear","DOI":"10.3166\/objet.9.4.95-114"},{"key":"58_CR10","doi-asserted-by":"crossref","unstructured":"Baar T, Beckert B, Schmitt PH (2001) An extension of Dynamic Logic for modelling OCL\u2019s @pre operator. In: Proceedings, Fourth Andrei Ershov International Conference, Perspectives of System Informatics, Novosibirsk, Russia, LNCS, vol 2244. Springer, pp 47\u201354","DOI":"10.1007\/3-540-45575-2_7"},{"key":"58_CR11","first-page":"In","volume":"UML","author":"Baar","year":"2000","unstructured":"Baar T, H\u00e4hnle R (2000) An integrated metamodel for OCL types. In: France R, Rumpe B, Whittle J (eds) Proc. OOPSLA 2000 Workshop Refactoring the UML: In Search of the Core, Minneapolis\/MI, USA, Oct.","journal-title":"OOPSLA 2000 Workshop Refactoring the"},{"key":"58_CR12","doi-asserted-by":"crossref","unstructured":"Baar T, H\u00e4hnle R, Sattler T, Schmitt PH (2000) Entwurfsmustergesteuerte Erzeugung von OCL-Constraints. In: Mehlhorn K, Snelting G (eds) Softwaretechnik-Trends, Informatik Aktuell, pp 389\u2013404. Springer-Verlag, Sept. In German.","DOI":"10.1007\/978-3-642-58322-3_30"},{"key":"58_CR13","doi-asserted-by":"crossref","unstructured":"Balser M, Reif W, Schellhorn G, Stenzel K, Thums A (2000) Formal system development with KIV. In: Maibaum T (ed) Fundamental Approaches to Software Engineering, LNCS, vol 1783. Springer-Verlag","DOI":"10.1007\/3-540-46428-X_25"},{"key":"58_CR14","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1109\/2.796139","volume":"32","author":"Beck","year":"1999","unstructured":"Beck K (1999) Embracing change with Extreme Programming. Computer 32:70\u201377, Oct.","journal-title":"Computer"},{"key":"58_CR15","unstructured":"Beckert B (2001) A dynamic logic for the formal verification of Java Card programs. In: Attali I, Jensen T (eds) Java on Smart Cards: Programming and Security. Revised Papers, Java Card 2000, International Workshop, Cannes, France, LNCS, vol 2041. Springer-Verlag, pp 6\u201324"},{"key":"58_CR16","unstructured":"Beckert B, Giese M, Habermalz E, H\u00e4hnle R, Roth A, R\u00fcmmer P, Schlager S (2004) Taclets: A new paradigm for writing theorem provers. Revista De La Real Academia De Ciencias Exactas, Fisicas Y Naturales. To appear."},{"key":"58_CR17","unstructured":"Beckert B, Keller U, Schmitt PH (2002) Translating the Object Constraint Language into first-order predicate logic. In: Proceedings, VERIFY, Workshop at Federated Logic Conferences (FLoC), Copenhagen, Denmark. Available at http:\/\/i12www.ira.uka.de\/\u223ckey\/doc\/2002\/BeckertKellerSchmitt02.ps.gz"},{"key":"58_CR18","doi-asserted-by":"crossref","unstructured":"Beckert B, Mostowski W (2003) A program logic for handling Java Card\u2019s transaction mechanism. In: Pezz\u00e8 M (ed) Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference, LNCS, vol 2621. Warsaw, Poland. Springer, pp 246\u2013260, April","DOI":"10.1007\/3-540-36578-8_18"},{"key":"58_CR19","doi-asserted-by":"crossref","unstructured":"Beckert B, Schlager S (2001) A sequent calculus for first-order dynamic logic with trace modalities. In: Gor\u00e8 R, Leitsch A, Nipkow T (eds) Proceedings, International Joint Conference on Automated Reasoning, Siena, Italy, LNCS vol 2083. Springer, pp 626\u2013641","DOI":"10.1007\/3-540-45744-5_51"},{"key":"58_CR20","doi-asserted-by":"crossref","unstructured":"Beckert B, Schlager S (2004) Software verification with integrated data type refinement for integer arithmetic. In: Proceedings, International Conference on Integrated Formal Methods, Canterbury, UK, LNCS. Springer. To appear","DOI":"10.1007\/978-3-540-24756-2_12"},{"key":"58_CR21","doi-asserted-by":"crossref","unstructured":"Beckert B, Schmitt PH (2003) Program verification using change information. In: Proceedings, Software Engineering and Formal Methods (SEFM), Brisbane, Australia. IEEE Press, pp 91\u201399","DOI":"10.1109\/SEFM.2003.1236211"},{"key":"58_CR22","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/2.59","volume":"21","author":"Boehm","year":"1988","unstructured":"Boehm BW (1988) A spiral model of software development and enhancement. IEEE Computer 21(5):61\u201372","journal-title":"IEEE Computer"},{"key":"58_CR23","unstructured":"Borland Together homepage. At http:\/\/www.borland.com\/together\/index.html"},{"key":"58_CR24","doi-asserted-by":"crossref","unstructured":"Breu R, Grosu R, Huber F, Rumpe B, Schwerin W (1997) Towards a precise semantics for object-oriented modeling techniques. In: Bosch J, Mitchell S (eds) Object-Oriented Technology, ECOOP\u201997 Post Conference Workshop Reader, Jyv\u00e4skyl\u00e4, Finland, LNCS, vol 1357. Springer-Verlag","DOI":"10.1007\/3-540-69687-3_42"},{"key":"58_CR25","doi-asserted-by":"crossref","unstructured":"Brucker AD, Wolff B (2002) HOL-OCL: Experiences, consequences and design choices. In: J\u00e9z\u00e9quel J-M, Hussmann H, Cook S (eds) UML 2002: Model Engineering, Concepts and Tools, LNCS, vol 2460. Springer-Verlag, pp 196\u2013211","DOI":"10.1007\/3-540-45800-X_17"},{"key":"58_CR26","doi-asserted-by":"crossref","unstructured":"Bubel R, H\u00e4hnle R (2003) Formal specification of security-critical railway software with the KeY system. In: Arts T, Fokkink W (eds) Proceedings, Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS), Electronic Notes in Theoretical Computer Science, vol 80. Elsevier","DOI":"10.1016\/S1571-0661(04)80806-5"},{"key":"58_CR27","first-page":"Architecture","volume":"Cards","author":"Chen","year":"2000","unstructured":"Chen Z (2000) Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide. Java Series. Addison-Wesley, June","journal-title":"Java Card Technology for Smart"},{"key":"58_CR28","first-page":"Object","volume":"Systems","author":"Cook","year":"1994","unstructured":"Cook S, Daniels J (1994) Designing Object Systems: Object-Oriented Modelling with Syntropy. The Object-Oriented Series. Prentice Hall","journal-title":"Designing Object"},{"key":"58_CR29","unstructured":"Crocker D (2002) Perfect Developer: A tool for rigorous object-oriented software development. In: Clark T, Evans A, Lano K (eds) Proc. Fourth Workshop on Rigorous Object-Oriented Methods, London"},{"key":"58_CR30","unstructured":"Darvas A, H\u00e4hnle R, Sands D (2003) A theorem proving approach to analysis of secure information flow. In: Gorrieri R (ed) Workshop on Issues in the Theory of Security (WITS). IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS"},{"key":"58_CR31","unstructured":"Dresden-OCL homepage. At http:\/\/dresden-ocl.sourceforge.net\/"},{"key":"58_CR32","unstructured":"Evans A, Bruel J-M, France R, Lano K, Rumpe B (1998) Making UML precise. In: Andrade L, Moreira A, Deshpande A, Kent S (eds) Proceedings of the OOPSLA\u201998 Workshop on Formalizing UML. Why? How?"},{"key":"58_CR33","unstructured":"Finger F (2000) Design and implementation of a modular OCL compiler. Diplomarbeit, Technische Universit\u00e4t Dresden, Fakult\u00e4t f\u00fcr Informatik, Mar."},{"key":"58_CR34","unstructured":"Fowler M, Scott K (1997) UML Destilled. Applying the Standard Object Modeling Language. Addison-Wesley"},{"key":"58_CR35","doi-asserted-by":"crossref","unstructured":"France R (1999) A problem-oriented analysis of basic UML static requirements modeling concepts. In: Proceedings of the 1999 ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications. ACM Press, pp 57\u201369","DOI":"10.1145\/320385.320390"},{"key":"58_CR36","unstructured":"Fujita H, Hasegawa R (1991) A model generation theorem prover in KL1 using a ramified-stack algorithm. In: Furukawa K (ed) Proceedings 8th International Conference on Logic Programming, Paris\/France. MIT Press, pp 535\u2013548"},{"key":"58_CR37","first-page":"Elements","volume":"Patterns","author":"Gamma","year":"1995","unstructured":"Gamma E, Helm R, Johnson R, Vlissides J (1995) Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading\/MA","journal-title":"Design"},{"key":"58_CR38","doi-asserted-by":"crossref","unstructured":"Giese M (2001) Incremental closure of free variable tableaux. In: Gor\u00e9, R., Leitsch A, Nipkow T (eds) Proc. Intl. Joint Conference on Automated Reasoning (IJCAR), Siena, Italy, LNCS, vol 2083. Springer-Verlag, pp 545\u2013560","DOI":"10.1007\/3-540-45744-5_46"},{"key":"58_CR39","unstructured":"Giese M (2003) Taclets and the KeY prover. In: L\u00fcth C, Aspinall D (eds) Intl., Workshop on User Interfaces for Theorem Provers, UITP 2003, Rome, Italy. Arcane, Rome, pp 74\u201380. Also as Tech. Report 189, Inst. f. Informatik, Albert-Ludwigs-Universit\u00e4t, Freiburg"},{"key":"58_CR40","unstructured":"Habermalz E (2000) Interactive theorem proving with schematic theory specific rules. Technical Report 19\/00, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe. Available at http:\/\/i12www.ira.uka.de\/\u223ckey\/doc\/2000\/stsr.ps.gz"},{"key":"58_CR41","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle R, Johannisson K, Ranta A (2002) An authoring tool for informal and formal requirements specifications. In: Kutsche R-D, Weber H (eds) Fundamental Approaches to Software Engineering (FASE), Part of Joint European Conferences on Theory and Practice of Software, ETAPS, Grenoble, LNCS, vol 2306. Springer-Verlag, pp 233\u2013248","DOI":"10.1007\/3-540-45923-5_16"},{"key":"58_CR42","doi-asserted-by":"crossref","unstructured":"Harel D (1984) Dynamic logic. In: Gabbay D, Guenthner F (eds) Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, chapter 10. Reidel, Dordrecht, pp 497\u2013604","DOI":"10.1007\/978-94-009-6259-0_10"},{"key":"58_CR43","doi-asserted-by":"crossref","unstructured":"Harel D, Kozen D, Tiuryn J (2000) Dynamic Logic. MIT Press","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"58_CR44","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (2001) Economics of software verification. In: Proc., Workshop on Program Analysis for Software Tools and Engineering, Snowbird, Utah, USA, ACM, June","DOI":"10.1145\/379605.379681"},{"key":"58_CR45","doi-asserted-by":"crossref","unstructured":"Hutter D, Langenstein B, Sengler C, Siekmann JH, Stephan W (1996) Deduction in the Verification Support Environment (VSE). In: Gaudel M-C, Woodcock J (eds) Proceedings, Formal Methods Europe: Industrial Benefits Advances in Formal Methods. Springer","DOI":"10.1007\/3-540-60973-3_92"},{"key":"58_CR46","unstructured":"Jacobson I, Rumbaugh J, Booch G (1999) The Unified Software Development Process. Object Technology Series. Addison-Wesley, Reading\/MA"},{"key":"58_CR47","unstructured":"JavaCC homepage. At http:\/\/www.webgain.com\/products\/java_cc\/"},{"key":"58_CR48","unstructured":"JUnit homepage. At http:\/\/junit.sourceforge.net\/"},{"key":"58_CR49","unstructured":"Keller U (2002) \u00dcbersetzung von OCL-Constraints in Formeln einer Dynamischen Logik f\u00fcr Java. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe. In German"},{"key":"58_CR50","unstructured":"Klebanov V (2003) Proof Re-Use in Java Software Verification. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe"},{"key":"58_CR51","doi-asserted-by":"crossref","unstructured":"Kozen D, Tiuryn J (1990) Logics of programs. In: van Leeuwen J (ed) Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 14. The MIT Press, pp 789\u2013840","DOI":"10.1016\/B978-0-444-88074-1.50019-6"},{"key":"58_CR52","unstructured":"Lano K, Clark D, Androutsopoulos K (2002) Formalising inter-model consistency of the UML. In: Kuzniarz L, Reggio G, Sourrouille JL, Huzar Z (eds) Blekinge Institute of Technology, Research Report 2002:06. UML 2002, Model Engineering, Concepts and Tools. Workshop on Consistency Problems in UML-based Software Development. Workshop Materials. Department of Software Engineering and Computer Science, Blekinge Institute of Technology, pp 133\u2013148"},{"key":"58_CR53","doi-asserted-by":"crossref","unstructured":"Larsson D, Mostowski W (2004) Specifying Java Card API in OCL. In: OCL 2.0 Workshop at UML 2003, ENTCS. Elsevier. To appear","DOI":"10.1016\/j.entcs.2003.09.001"},{"key":"58_CR54","unstructured":"Mellor SJ, D\u2019Souza D, Clark T, Evans A, Kent S (2001) Infrastructure and Superstructure of the Unified Modeling Language 2.0 (Response to UML2.0 RfP). Technical report, Submission to the OMG"},{"key":"58_CR55","unstructured":"Meyer B (1997) Object-Oriented Software Construction. Prentice-Hall, Englewood Cliffs, second edition"},{"key":"58_CR56","unstructured":"Mostowski W (2002) Rigorous development of JavaCard applications. In: Clark T, Evans A, Lano K (eds) Proc. Fourth Workshop on Rigorous Object-Oriented Methods, London. Available at http:\/\/www.cs.chalmers.se\/\u223cwoj\/papers\/room2002.ps.gz"},{"key":"58_CR57","unstructured":"Response to the UML OCL RfP (2002) June. OMG document ad\/2002-05-09"},{"key":"58_CR58","unstructured":"Object Modeling Group (2003) Unified Modelling Language Specification, version 1.5, Mar."},{"key":"58_CR59","doi-asserted-by":"crossref","unstructured":"Owre S, Rajan S, Rushby J, Shankar N, Srivas M (1996) PVS: Combining specification, proof checking, and model checking. In: Alur R, Henzinger TA (eds) Computer-Aided Verification, CAV \u201996, LNCS, vol 1102. Springer-Verlag, pp 411\u2013414, July\/August","DOI":"10.1007\/3-540-61474-5_91"},{"key":"58_CR60","doi-asserted-by":"crossref","unstructured":"Paulson LC (1994) Isabelle: a generic theorem prover, LNCS, vol 828. Springer-Verlag","DOI":"10.1007\/BFb0030541"},{"key":"58_CR61","doi-asserted-by":"crossref","unstructured":"Pratt VR (1977) Semantical considerations on Floyd-Hoare logic. In: Proceedings, 18th Annual IEEE Symposium on Foundation of Computer Science","DOI":"10.1109\/SFCS.1976.27"},{"key":"58_CR62","unstructured":"Recoder homepage. http:\/\/recoder.sourceforge.net\/"},{"key":"58_CR63","unstructured":"Richters M (2002) A Precise Approach to Validating UML Models and OCL Constraints, BISS Monographs, vol 14. Logos Verlag. PhD thesis, Universit\u00e4t Bremen"},{"key":"58_CR64","unstructured":"Roth A (2002) Deduktiver Softwareentwurf am Beispiel des Java Collections Frameworks. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, June. In German"},{"key":"58_CR65","unstructured":"Schmitt PH (2001) A model theoretic semantics of OCL. In: Beckert B, France R, H\u00e4hnle R, Jacobs B (eds) Proceedings, IJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development, Siena, Italy. Technical Report DII 07\/01, Dipartimento di Ingegneria dell\u2019Informazione, Universit\u00e0 degli Studi di Siena, pp 43\u201357"},{"key":"58_CR66","unstructured":"Snook C, Wheeler P, Butler M (2003) Preliminary tool extensions for integration of UML and B. IST-2000-30103 project deliverable D4.1.2. Available at http:\/\/www.keesda.com\/pussee\/"},{"key":"58_CR67","unstructured":"Stenzel K (2001) Verification of java card programs. Technical report 2001-5, Institut f\u00fcr Informatik, Universit\u00e4t Augsburg, Germany. Available at http:\/\/www.Informatik.Uni-Augsburg.de\/swt\/fmg\/papers\/"},{"key":"58_CR68","unstructured":"Sun Microsystems, Inc. (2001) Java Card 2.0 Language Subset and Virtual Machine Specification, Palo Alto\/CA, Oct."},{"key":"58_CR69","unstructured":"Sun Microsystems, Inc. (2002) Java Card 2.2 Platform Specification, Palo Alto\/CA, USA, Sept."},{"key":"58_CR70","unstructured":"von Oheimb D (2000) Axiomatic semantics for Java light . In: Drossopoulou S, Eisenbach S, Jacobs B, Leavens GT, M\u00fcller P, Poetzsch-Heffter A (eds) Proceedings, Formal Techniques for Java Programs, Workshop at ECOOP\u201900, Cannes, France"},{"key":"58_CR71","doi-asserted-by":"crossref","unstructured":"von Oheimb D (2001) Analyzing Java in Isabelle\/HOL. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Jan.","DOI":"10.1002\/cpe.598"},{"key":"58_CR72","unstructured":"Warmer J, Kleppe A (1999) OCL: The constraint language of the UML. Journal of Object-Oriented Programming, 12(1):10\u201313,28, Mar."}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-004-0058-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-004-0058-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-004-0058-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T21:11:02Z","timestamp":1585689062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-004-0058-x"}},"subtitle":["Integrating object oriented design and formal verification"],"short-title":[],"issued":{"date-parts":[[2005,2]]},"references-count":72,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,2]]}},"alternative-id":["58"],"URL":"https:\/\/doi.org\/10.1007\/s10270-004-0058-x","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,2]]}}}