{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T17:18:13Z","timestamp":1764350293865,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496640"},{"type":"electronic","value":"9783662496657"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49665-7_23","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T08:09:42Z","timestamp":1458547782000},"page":"383-400","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique"],"prefix":"10.1007","author":[{"given":"Sander","family":"de Putter","sequence":"first","affiliation":[]},{"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"23_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.5381\/jot.2015.14.3.a1","volume":"14","author":"M Amrani","year":"2015","unstructured":"Amrani, M., Combemale, B., L\u00facio, L., Selim, G.M.K., Dingel, J., Le Traon, Y., Vangheluwe, H., Cordy, J.R.: Formal verification techniques for model transformations: a tridimensional classification. JOT 14(3), 1\u201343 (2015)","journal-title":"JOT"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-73859-6_9","volume-title":"Algebra and Coalgebra in Computer Science","author":"P Baldan","year":"2007","unstructured":"Baldan, P., Corradini, A., Ehrig, H., Heckel, R., K\u00f6nig, B.: Bisimilarity and behaviour-preserving reconfigurations of open petri nets. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 126\u2013142. Springer, Heidelberg (2007)"},{"key":"23_CR3","first-page":"106-1","volume-title":"Computer Science Handbook Chap. 106","author":"J Bowen","year":"2004","unstructured":"Bowen, J., Hinchey, M.: Formal methods. In: Tucker, A.B. (ed.) Computer Science Handbook Chap. 106, pp. 106-1\u2013106-25. ACM, New York (2004)"},{"key":"23_CR4","unstructured":"Giese, H., Glesner, S., Leitner, J., Sch\u00e4fer, W., Wagner, R.: Towards verified model transformations. In: MoDeVVa 2006, pp. 78\u201393 (2006)"},{"issue":"3","key":"23_CR5","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ Glabbeek van","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555\u2013600 (1996)","journal-title":"J. ACM"},{"key":"23_CR6","volume-title":"MDA Explained: The Model Driven Architecture(TM): Practice and Promise","author":"A Kleppe","year":"2005","unstructured":"Kleppe, A., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture(TM): Practice and Promise. Addison-Wesley Professional, Boston (2005)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/11888116_13","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"F Lang","year":"2006","unstructured":"Lang, F.: Refined interfaces for compositional verification. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 159\u2013174. Springer, Heidelberg (2006)"},{"issue":"4","key":"23_CR8","first-page":"1","volume":"9","author":"F Lang","year":"2013","unstructured":"Lang, F., Mateescu, R.: partial model checking using networks of labelled transition systems and boolean equation systems. Log. Methods Comput. Sci. 9(4), 1\u201332 (2013)","journal-title":"Log. Methods Comput. Sci."},{"issue":"3","key":"23_CR9","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1016\/j.scico.2014.04.004","volume":"96","author":"R Mateescu","year":"2014","unstructured":"Mateescu, R., Wijs, A.: Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci. Comput. Prog. 96(3), 354\u2013376 (2014)","journal-title":"Sci. Comput. Prog."},{"key":"23_CR10","unstructured":"de Putter, S.: Coq code proving the correctness of the LTS transformation verification technique (2015). http:\/\/www.mdsetechnology.org\/attachments\/article\/2\/FASE16_property_preservation.zip"},{"key":"23_CR11","first-page":"1","volume":"14","author":"LA Rahim","year":"2013","unstructured":"Rahim, L.A., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14, 1\u201326 (2013). http:\/\/dx.doi.org\/10.1007\/s10270-013-0358-0","journal-title":"Softw. Syst. Model."},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-540-77050-3_17","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"D Saha","year":"2007","unstructured":"Saha, D.: An incremental bisimulation algorithm. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 204\u2013215. Springer, Heidelberg (2007)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-3-319-09108-2_8","volume-title":"Graph Transformation","author":"GMK Selim","year":"2014","unstructured":"Selim, G.M.K., L\u00facio, L., Cordy, J.R., Dingel, J., Oakes, B.J.: Specification and verification of graph-based model transformation properties. In: Giese, H., K\u00f6nig, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 113\u2013129. Springer, Heidelberg (2014)"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-58179-0_67","volume-title":"Computer Aided Verification","author":"O Sokolsky","year":"1994","unstructured":"Sokolsky, O., Smolka, S.: Incremental model checking in the modal mu-calculus. In: Dill, D.L. (ed.) Computer Aided Verification. LNCS, vol. 818, pp. 351\u2013363. Springer, Heidelberg (1994)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-642-24485-8_39","volume-title":"Model Driven Engineering Languages and Systems","author":"K Stenzel","year":"2011","unstructured":"Stenzel, K., Moebius, N., Reif, W.: Formal verification of QVT transformations for code generation. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 533\u2013547. Springer, Heidelberg (2011)"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Swamy, G.: Incremental methods for formal verification and logic synthesis. Ph.D. thesis, University of California (1996)","DOI":"10.2139\/ssrn.3702088"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/978-3-319-07602-7_21","volume-title":"Formal Aspects of Component Software","author":"A Wijs","year":"2014","unstructured":"Wijs, A.: Define, verify, refine: correct composition and transformation of concurrent system semantics. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 348\u2013368. Springer, Heidelberg (2014)"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Wijs, A.J.: Confluence detection for transformations of labelled transition systems. In: GaM 2015. EPTCS, vol. 181, pp. 1\u201315. Open Publishing Association (2015)","DOI":"10.4204\/EPTCS.181.1"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/978-3-642-36742-7_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Wijs","year":"2013","unstructured":"Wijs, A., Engelen, L.: Efficient property preservation checking of model refinements. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 565\u2013579. Springer, Heidelberg (2013)"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-319-06200-6_21","volume-title":"NASA Formal Methods","author":"A Wijs","year":"2014","unstructured":"Wijs, A., Engelen, L.: REFINER: towards formal verification of model transformations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 258\u2013263. Springer, Heidelberg (2014)"},{"issue":"1\u20132","key":"23_CR21","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/0890-5401(90)90058-P","volume":"87","author":"G Winskel","year":"1990","unstructured":"Winskel, G.: A Compositional proof system on a category of labelled transition systems. Inf. Comput. 87(1\u20132), 2\u201357 (1990)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49665-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,15]],"date-time":"2022-06-15T19:16:15Z","timestamp":1655320575000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49665-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496640","9783662496657"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49665-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}