{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T09:32:14Z","timestamp":1780392734856,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642244841","type":"print"},{"value":"9783642244858","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24485-8_39","type":"book-chapter","created":{"date-parts":[[2011,10,10]],"date-time":"2011-10-10T15:59:05Z","timestamp":1318262345000},"page":"533-547","source":"Crossref","is-referenced-by-count":15,"title":["Formal Verification of QVT Transformations for Code Generation"],"prefix":"10.1007","author":[{"given":"Kurt","family":"Stenzel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nina","family":"Moebius","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"39_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Balser","year":"2000","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: FASE 2000. LNCS, vol.\u00a01783, p. 363. Springer, Heidelberg (2000)"},{"key":"39_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"39_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-00593-0_2","volume-title":"Fundamental Approaches to Software Engineering","author":"A. Boronat","year":"2009","unstructured":"Boronat, A., Heckel, R., Meseguer, J.: Rewriting logic semantics and verification of model transformations. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 18\u201333. Springer, Heidelberg (2009)"},{"key":"39_CR4","unstructured":"Brucker, A.D., Wolff, B.: The HOL-OCL book. Technical Report 525, ETH Z\u00fcrich (2006)"},{"key":"39_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-01648-6_28","volume-title":"Models in Software Engineering","author":"F. B\u00fcttner","year":"2009","unstructured":"B\u00fcttner, F., Kuhlmann, M.: Shortcomings of the embedding of OCL into QVT imperativeOCL. In: Chaudron, M.R.V. (ed.) MODELS 2008. LNCS, vol.\u00a05421, pp. 263\u2013272. Springer, Heidelberg (2009)"},{"key":"39_CR6","doi-asserted-by":"crossref","unstructured":"Czarnecki, K., Helsen, S.: Feature-based survey of model transformation approaches. IBM Systems Journal\u00a045(3) (2006)","DOI":"10.1147\/sj.453.0621"},{"key":"39_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-04425-0_19","volume-title":"Model Driven Engineering Languages and Systems","author":"J. Lara de","year":"2009","unstructured":"de Lara, J., Guerra, E.: Formal support for QVT-relations with coloured petri nets. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol.\u00a05795, pp. 256\u2013270. Springer, Heidelberg (2009)"},{"key":"39_CR8","volume-title":"Fundamentals of algebraic graph transformation","author":"H. Ehrig","year":"2006","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of algebraic graph transformation. Springer, Heidelberg (2006)"},{"key":"39_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-69100-6_7","volume-title":"Model Driven Architecture \u2013 Foundations and Applications","author":"G. Engels","year":"2008","unstructured":"Engels, G., Kleppe, A., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: From UML activities to TAAL - towards behaviour-preserving model transformations. In: Schieferdecker, I., Hartman, A. (eds.) ECMDA-FA 2008. LNCS, vol.\u00a05095, pp. 94\u2013109. Springer, Heidelberg (2008)"},{"key":"39_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-01924-1_13","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2009","author":"L. Favre","year":"2009","unstructured":"Favre, L.: A formal foundation for metamodeling. In: Kordon, F., Kermarrec, Y. (eds.) Ada-Europe 2009. LNCS, vol.\u00a05570, pp. 177\u2013191. Springer, Heidelberg (2009)"},{"key":"39_CR11","unstructured":"Giese, H., Glesner, S., Leitner, J., Sch\u00e4fer, W., Wagner, R.: Towards verified model transformations. In: Proceedings of the MoDeVa Workshop at MoDELS 2006 (2006)"},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"Gogolla, M., B\u00fcttner, F., Richters, M.: USE: A UML-Based Specification Environment for Validating UML and OCL. Science of Computer Programming\u00a069 (2007)","DOI":"10.1016\/j.scico.2007.01.013"},{"key":"39_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-72952-5_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"H. Grandy","year":"2007","unstructured":"Grandy, H., Stenzel, K., Reif, W.: A refinement method for java programs. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol.\u00a04468, pp. 221\u2013235. Springer, Heidelberg (2007)"},{"key":"39_CR14","unstructured":"Object\u00a0Management Group. Object Constraint Language, Version 2.3 (2010)"},{"key":"39_CR15","unstructured":"Object\u00a0Management Group. Meta Object Facility (MOF) 2.0 Query\/View\/Transformation Specification, Version 1.1 (2011)"},{"key":"39_CR16","unstructured":"Haneberg, D., B\u00e4umler, S., Balser, M., Grandy, H., Ortmeier, F., Reif, W., Schellhorn, G., Schmitt, J., Stenzel, K.: The User Interface of the KIV Verification System \u2014 A System Description. Electronic Notes in Theoretical Computer Science UITP Special Issue (2006)"},{"key":"39_CR17","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"39_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination. In: FASE 2000. LNCS, vol.\u00a01783, pp. 284\u2013303. Springer, Heidelberg (2000)"},{"key":"39_CR19","unstructured":"KIV homepage, http:\/\/www.informatik.uni-augsburg.de\/swt\/kiv"},{"key":"39_CR20","unstructured":"Krieger, M., Knapp, A.: Executing underspecified OCL operation contracts with a SAT solver. In: Proceedings of the 8th International Workshop on OCL Concepts and Tools (OCL 2008) at MoDELS 2008. Electronic Communications of the EASST, vol.\u00a015 (2008)"},{"key":"39_CR21","unstructured":"Lano, K.: Using B to verify UML transformations. In: Proceedings of the MoDeVa Workshop at MoDELS 2006 (2006)"},{"key":"39_CR22","volume-title":"Workshop on Secure Software Engineering, SecSE, at ARES 2009","author":"N. Moebius","year":"2009","unstructured":"Moebius, N., Stenzel, K., Grandy, H., Reif, W.: SecureMDD: A Model-Driven Development Method for Secure Smart Card Applications. In: Workshop on Secure Software Engineering, SecSE, at ARES 2009. IEEE Press, Los Alamitos (2009)"},{"key":"39_CR23","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Modeling Security-Critical Applications with UML in the SecureMDD Approach. International Journal On Advances in Software\u00a01(1) (2008)"},{"key":"39_CR24","doi-asserted-by":"crossref","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Generating formal specifications for security-critical applications - a model-driven approach. In: ICSE 2009 Workshop: International Workshop on Software Engineering for Secure Systems (SESS 2009), IEEE\/ACM Digital Libary (2009)","DOI":"10.1109\/IWSESS.2009.5068461"},{"key":"39_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-11747-3_13","volume-title":"Engineering Secure Software and Systems","author":"N. Moebius","year":"2010","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Formal verification of application-specific security properties in a model-driven approach. In: Massacci, F., Wallach, D., Zannone, N. (eds.) ESSoS 2010. LNCS, vol.\u00a05965, pp. 166\u2013181. Springer, Heidelberg (2010)"},{"key":"39_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-03741-2_26","volume-title":"Algebra and Coalgebra in Computer Science","author":"F. Orejas","year":"2009","unstructured":"Orejas, F., Guerra, E., de Lara, J., Ehrig, H.: Correctness, completeness and termination of pattern-based model-to-model transformation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 383\u2013397. Springer, Heidelberg (2009)"},{"key":"39_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-04164-8_8","volume-title":"Semantics and Algebraic Specification","author":"F. Orejas","year":"2009","unstructured":"Orejas, F., Wirsing, M.: On the specification and verification of model transformations. In: Palsberg, J. (ed.) Semantics and Algebraic Specification. LNCS, vol.\u00a05700, pp. 140\u2013161. Springer, Heidelberg (2009)"},{"key":"39_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-642-16373-9_32","volume-title":"Conceptual Modeling \u2013 ER 2010","author":"A. Queralt","year":"2010","unstructured":"Queralt, A., Rull, G., Teniente, E., Farr\u00e9, C., Urp\u00ed, T.: AuRUS: Automated Reasoning on UML\/OCL Schemas. In: Parsons, J., Saeki, M., Shoval, P., Woo, C., Wand, Y. (eds.) ER 2010. LNCS, vol.\u00a06412, pp. 438\u2013444. Springer, Heidelberg (2010)"},{"key":"39_CR29","unstructured":"QVT Operational (Eclipse Project), http:\/\/www.eclipse.org\/projects\/project_summary.php?projectid=modeling.m2m.qvt-oml ."},{"key":"39_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-16145-2_12","volume-title":"Model Driven Engineering Languages and Systems","author":"L. Ab Rahim","year":"2010","unstructured":"Ab Rahim, L., Whittle, J.: Verifying semantic conformance of state machine-to-java code generators. In: Petriu, D.C., Rouquette, N., Haugen, \u00d8. (eds.) MODELS 2010. LNCS, vol.\u00a06394, pp. 166\u2013180. Springer, Heidelberg (2010)"},{"key":"39_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-540-69927-9_10","volume-title":"Theory and Practice of Model Transformations","author":"R. Romeikat","year":"2008","unstructured":"Romeikat, R., Roser, S., M\u00fcllender, P., Bauer, B.: Translation of QVT relations into QVT operational mappings. In: Vallecillo, A., Gray, J., Pierantonio, A. (eds.) ICMT 2008. LNCS, vol.\u00a05063, pp. 137\u2013151. Springer, Heidelberg (2008)"},{"key":"39_CR32","unstructured":"SmartQVT, http:\/\/sourceforge.net\/projects\/smartqvt\/"},{"key":"39_CR33","volume-title":"Proc. Design, Automation and Test in Europe\u00a0(DATE 2010)","author":"M. Soeken","year":"2010","unstructured":"Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML\/OCL Models Using Boolean Satisfiability. In: Proc. Design, Automation and Test in Europe\u00a0(DATE 2010). IEEE, Los Alamitos (2010)"},{"key":"39_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine: Definition, Verification, Validation","author":"R.F. St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R.F., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)"},{"key":"39_CR35","volume-title":"EMF Eclipse Modeling Framework","author":"D. Steinberg","year":"2009","unstructured":"Steinberg, D., Budensky, F., Paternostro, M., Merks, E.: EMF Eclipse Modeling Framework, 2nd edn. Addison-Wesley, Reading (2009)","edition":"2"},{"key":"39_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-27815-3_37","volume-title":"Algebraic Methodology and Software Technology","author":"K. Stenzel","year":"2004","unstructured":"Stenzel, K.: A formally verified calculus for full java card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 491\u2013505. Springer, Heidelberg (2004)"},{"key":"39_CR37","unstructured":"Stenzel, K.: Verification of Java Card Programs. PhD thesis, Faculty of Informatics, Augsburg University, Germany (2005)"},{"key":"39_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-13688-7_16","volume-title":"Theory and Practice of Model Transformations","author":"J. Troya","year":"2010","unstructured":"Troya, J., Vallecillo, A.: Towards a rewriting logic semantics for ATL. In: Tratt, L., Gogolla, M. (eds.) ICMT 2010. LNCS, vol.\u00a06142, pp. 230\u2013244. Springer, Heidelberg (2010)"},{"key":"39_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-48737-9_4","volume-title":"Formal Syntax and Semantics of Java","author":"D. Oheimb von","year":"1999","unstructured":"von Oheimb, D., Nipkow, T.: Machine-checking the java specification: Proving type-safety. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523, pp. 119\u2013156. Springer, Heidelberg (1999)"},{"key":"39_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1007\/978-3-642-04425-0_59","volume-title":"Model Driven Engineering Languages and Systems","author":"M. Wimmer","year":"2009","unstructured":"Wimmer, M., Kusel, A., Schoenboeck, J., Kappel, G., Retschitzegger, W., Schwinger, W.: Reviving QVT relations: Model-based debugging using colored petri nets. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol.\u00a05795, pp. 727\u2013732. Springer, Heidelberg (2009)"},{"key":"39_CR41","unstructured":"XPand, http:\/\/wiki.eclipse.org\/Xpand"}],"container-title":["Lecture Notes in Computer Science","Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24485-8_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,17]],"date-time":"2019-06-17T04:32:53Z","timestamp":1560745973000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24485-8_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642244841","9783642244858"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24485-8_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}