{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T19:14:09Z","timestamp":1775243649833,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030021450","type":"print"},{"value":"9783030021467","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-030-02146-7_15","type":"book-chapter","created":{"date-parts":[[2018,10,5]],"date-time":"2018-10-05T21:44:02Z","timestamp":1538775842000},"page":"288-296","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["The SLCO Framework for Verified, Model-Driven Construction of Component Software"],"prefix":"10.1007","author":[{"given":"Sander","family":"de Putter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,5]]},"reference":[{"key":"15_CR1","unstructured":"Abrial, J.R., Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-30476-7_5","volume-title":"Theory and Practice of Model Transformations","author":"S Andova","year":"2012","unstructured":"Andova, S., van den Brand, M.G.J., Engelen, L.: Reusable and correct endogenous model transformations. In: Hu, Z., de Lara, J. (eds.) ICMT 2012. LNCS, vol. 7307, pp. 72\u201388. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30476-7_5"},{"key":"15_CR3","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The vercors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"issue":"6","key":"15_CR5","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1145\/3140587.3062358","volume":"52","author":"Timothy Bourke","year":"2017","unstructured":"Bourke, T., Brun, L., Dagand, P.E., Leroy, X., Pouzet, M., Rieg, L.: A formally verified compiler for lustre. In: PLDI, pp. 586\u2013601. ACM SIGPLAN Notices. ACM, New York (2017)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-319-28934-2_8","volume-title":"Formal Aspects of Component Software","author":"Dragan Bo\u0161na\u010dki","year":"2016","unstructured":"Bo\u0161na\u010dki, D., et al.: Towards modular verification of threaded concurrent executable code generated from DSL models. In: Braga, C., \u00d6lveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 141\u2013160. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-28934-2_8"},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Sjoerd Cranen","year":"2013","unstructured":"Cranen, S., et al.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199\u2013213. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_15"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.knosys.2016.10.023","volume":"115","author":"I. Dejanovi\u0107","year":"2017","unstructured":"Dejanovi\u0107, I., Vaderna, R., Milosavljevi\u0107, G., Vukovi\u0107, \u017d.: TextX: a python tool for Domain-Specific Languages implementation. Knowl.-Based Syst. 115, 1\u20134 (2017)","journal-title":"Knowledge-Based Systems"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Deligiannis, P., Donaldson, A., Ketema, J., Lal, A., Thomson, P.: Asynchronous programming, analysis and testing with state machines. In: PLD, vol. 50, pp. 154\u2013164. ACM SIGPLAN Notices. ACM Press (2015)","DOI":"10.1145\/2813885.2737996"},{"key":"15_CR10","unstructured":"Dormoy, F.X.: Scade 6: a model based solution for safety critical software development. In: ERTS, pp. 1\u20139 (2008)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-319-10181-1_20","volume-title":"Integrated Formal Methods","author":"A F\u00fcrst","year":"2014","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D., Desai, K., Sato, N., Miyazaki, K.: Code generation for event-B. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 323\u2013338. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_20"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Hindman, B., Grossman, D.: Atomicity via source-to-source translation. In: MSPC, pp. 82\u201391. ACM Press (2006)","DOI":"10.1145\/1178597.1178611"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Narayanan, A., Karsai, G.: Towards verifying model transformations. In: GT-VMT. ENTCS, vol. 211, pp. 191\u2013200. Elsevier (2008)","DOI":"10.1016\/j.entcs.2008.04.041"},{"issue":"2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s10515-012-0116-5","volume":"20","author":"Colin O\u2019Halloran","year":"2012","unstructured":"O\u2019Halloran, C.: Automated verification of code automatically generated from simulink\u00ae. Autom. Softw. Eng. 20(2), 237\u2013264 (2013)","journal-title":"Automated Software Engineering"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"de Putter, S., Wijs, A.: A formal verification technique for behavioural model-to-model transformations. Form. Asp. Comput. 30(1), 3\u201343 (2017)","DOI":"10.1007\/s00165-017-0437-z"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-319-68034-7_7","volume-title":"Formal Aspects of Component Software","author":"S Putter de","year":"2017","unstructured":"de Putter, S., Wijs, A.: Compositional model checking is lively. In: Proen\u00e7a, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 117\u2013136. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68034-7_7"},{"key":"15_CR18","unstructured":"de Putter, S., Wijs, A., Zhang, D.: Model Driven Avoidance of Atomicity Violations under Relaxed-Memory Models (2018, Submitted)"},{"key":"15_CR19","unstructured":"Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Software and Systems Modeling pp. 1\u201326 (2013)"},{"issue":"6","key":"15_CR20","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1145\/2184319.2184345","volume":"55","author":"Tiark Rompf","year":"2012","unstructured":"Rompf, T., Odersky, M.: Lightweight Modular Staging: A Pragmatic Approach to Runtime Code Generation and Compiled DSLs. Commun. ACM 55(6), 121\u2013130 (2012)","journal-title":"Communications of the ACM"},{"key":"15_CR21","unstructured":"The MathWorks Inc., Simulink\u00ae. www.mathworks.com\/products\/simulink"},{"key":"15_CR22","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. LNCS, vol. 7795, pp. 565\u2013579. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_41"},{"key":"15_CR23","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, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_21"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Wijs, A.: Achieving discrete relative timing with untimed process algebra. In: ICECCS, pp. 35\u201344. IEEE (2007)","DOI":"10.1109\/ICECCS.2007.13"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Wijs, A., Fokkink, W.: From $$\\chi _{\\mathit{t}}$$ to $$\\mu $$CRL: combining performance and functional analysis. In: ICECCS, pp. 184\u2013193. IEEE (2005)","DOI":"10.1109\/ICECCS.2005.51"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1007\/978-3-319-48989-6_42","volume-title":"FM 2016: Formal Methods","author":"A Wijs","year":"2016","unstructured":"Wijs, A., Neele, T., Bo\u0161na\u010dki, D.: GPUexplore 2.0: unleashing GPU explicit-state model checking. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 694\u2013701. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_42"},{"key":"15_CR27","unstructured":"Zhang, D.: From Concurrent State Machines to Reliable Multi-threaded Java Code. Ph.D. thesis, Eindhoven University of Technology (2018)"},{"key":"15_CR28","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-66302-9_13","volume-title":"Communications in Computer and Information Science","author":"Dan Zhang","year":"2017","unstructured":"Zhang, D., et al.: Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations. In: Hammoudi, S., Pires, L.F., Selic, B., Desfray, P. (eds.) MODELSWARD 2016. CCIS, vol. 692, pp. 249\u2013273. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66302-9_13"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02146-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T18:41:26Z","timestamp":1775241686000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02146-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030021450","9783030021467"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02146-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"FACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Aspects of Component Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pohang","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Korea (Republic of)","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"facs2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sevlab.postech.ac.kr\/facs18","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}