{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:58:17Z","timestamp":1761929897040},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319663012"},{"type":"electronic","value":"9783319663029"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66302-9_13","type":"book-chapter","created":{"date-parts":[[2017,9,11]],"date-time":"2017-09-11T09:33:55Z","timestamp":1505122435000},"page":"249-273","source":"Crossref","is-referenced-by-count":5,"title":["Verifying Atomicity Preservation and Deadlock Freedom of a Generic Shared Variable Mechanism Used in Model-To-Code Transformations"],"prefix":"10.1007","author":[{"given":"Dan","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"van den Brand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cornelis","family":"Huizing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruurd","family":"Kuiper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,10]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1119479.1119480","volume":"28","author":"M Abadi","year":"2006","unstructured":"Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: static race detection for java. ACM Trans. Program. Lang. Syst. 28(2), 207\u2013255 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Biswas, S., Huang, J., Sengupta, A., Bond, M.D.: DoubleChecker: efficient sound and precise atomicity checking. In: ACM SIGPLAN Notices, vol. 49, pp. 28\u201339. ACM (2014)","DOI":"10.1145\/2666356.2594323"},{"key":"13_CR3","unstructured":"Blech, J., Glesner, S., Leitner, J.: Formal verification of java code generation from UML models. In: Fujaba Days, pp. 49\u201356 (2005)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-319-28934-2_8","volume-title":"Formal Aspects of Component Software","author":"D Bo\u0161na\u010dki","year":"2016","unstructured":"Bo\u0161na\u010dki, D., Brand, M., Gabriels, J., Jacobs, B., Kuiper, R., Roede, S., Wijs, A., Zhang, D.: 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). doi:\n10.1007\/978-3-319-28934-2_8"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE, pp. 385\u2013395. IEEE (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Choi, J.D., Lee, K., Loginov, A., O\u2019Callahan, R., Sarkar, V., Sridharan, M.: Efficient and precise datarace detection for multithreaded object-oriented programs. In: ACM SIGPLAN Notices, vol. 37, pp. 258\u2013269. ACM (2002)","DOI":"10.1145\/512529.512560"},{"key":"13_CR7","unstructured":"Engelen, L.: From Napkin sketches to reliable software. Ph.D. thesis, Eindhoven University of Technology (2012)"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: ACM SIGOPS Operating Systems Review, vol. 37, pp. 237\u2013252. ACM (2003)","DOI":"10.1145\/945445.945468"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/11817963_30","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2006","unstructured":"Farzan, A., Madhusudan, P.: Causal atomicity. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 315\u2013328. Springer, Heidelberg (2006). doi:\n10.1007\/11817963_30"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: ACM SIGPLAN Notices, vol. 38, pp. 338\u2013349. ACM (2003)","DOI":"10.1145\/781131.781169"},{"issue":"2","key":"13_CR11","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1147\/sj.72.0074","volume":"7","author":"JW Havender","year":"1968","unstructured":"Havender, J.W.: Avoiding deadlock in multitasking systems. IBM Syst. J. 7(2), 74\u201384 (1968)","journal-title":"IBM Syst. J."},{"key":"13_CR12","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). doi:\n10.1007\/978-3-642-20398-5_4"},{"key":"13_CR13","unstructured":"Jacobs, B., Bosnacki, D., Kuiper, R.: Modular termination verification: extended version. Technical report, Department of Computer Science, KU Leuven (2015)"},{"issue":"4","key":"13_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 1\u201354 (2009)","journal-title":"ACM Comput. Surv."},{"key":"13_CR15","volume-title":"MDA Explained: the Model Driven Architecture: Practice and Promise","author":"A Kleppe","year":"2005","unstructured":"Kleppe, A., Warmer, J., Bast, W.: MDA Explained: the Model Driven Architecture: Practice and Promise. Addison-Wesley Professional, Boston (2005)"},{"key":"13_CR16","unstructured":"Kolovos, D., Rose, L., Garca-Dominguez, A., Paige, R.: The Epsilon Book. Eclipse (2011)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-11957-6_22","volume-title":"Programming Languages and Systems","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Deadlock-free channels and locks. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 407\u2013426. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-11957-6_22"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). doi:\n10.1007\/3-540-44802-0_1"},{"issue":"5","key":"13_CR19","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-662-49665-7_23","volume-title":"Fundamental Approaches to Software Engineering","author":"S Putter","year":"2016","unstructured":"Putter, S., Wijs, A.: Verifying a verifier: on the formal correctness of an LTS transformation verification technique. In: Stevens, P., W\u0105sowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 383\u2013400. Springer, Heidelberg (2016). doi:\n10.1007\/978-3-662-49665-7_23"},{"issue":"2","key":"13_CR21","doi-asserted-by":"crossref","first-page":"1003","DOI":"10.1007\/s10270-013-0358-0","volume":"14","author":"L Rahim","year":"2015","unstructured":"Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003\u20131028 (2015)","journal-title":"Softw. Syst. Model."},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"13_CR23","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). doi:\n10.1007\/978-3-642-24485-8_39"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-642-03359-9_32","volume-title":"Theorem Proving in Higher Order Logics","author":"T Tuerk","year":"2009","unstructured":"Tuerk, T.: A formalisation of smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469\u2013484. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-03359-9_32"},{"issue":"2","key":"13_CR25","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). doi:\n10.1007\/978-3-319-07602-7_21"},{"key":"13_CR27","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). doi:\n10.1007\/978-3-642-36742-7_41"},{"key":"13_CR28","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). doi:\n10.1007\/978-3-319-06200-6_21"},{"key":"13_CR29","unstructured":"Zhang, D., Bo\u0161na\u010dki, D., van den Brand, M., Engelen, L., Huizing, C., Kuiper, R., Wijs, A.: Towards verified java code generation from concurrent state machines. In: AMT. CEUR Workshop Proceedings, vol. 1277, pp. 64\u201369. CEUR-WS.org (2014)"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Zhang, D., Bo\u0161na\u010dki, D., van den Brand, M., Huizing, C., Jacobs, B., Kuiper, R., Wijs, A.: Verification of atomicity preservation in model-to-code transformations. In: Fourth International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), pp. 578\u2013588. SCITEPRESS (2016)","DOI":"10.5220\/0005689405780588"}],"container-title":["Communications in Computer and Information Science","Model-Driven Engineering and Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66302-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,11]],"date-time":"2017-09-11T09:40:45Z","timestamp":1505122845000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66302-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319663012","9783319663029"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66302-9_13","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2017]]}}}