{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:56:24Z","timestamp":1761929784931,"version":"3.41.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319289335"},{"type":"electronic","value":"9783319289342"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-28934-2_8","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T15:32:56Z","timestamp":1453995176000},"page":"141-160","source":"Crossref","is-referenced-by-count":6,"title":["Towards Modular Verification of Threaded Concurrent Executable Code Generated from DSL Models"],"prefix":"10.1007","author":[{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"van den Brand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost","family":"Gabriels","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":"Sybren","family":"Roede","sequence":"additional","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":[[2016,1,29]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"van Amstel, M., van den Brand, M., Engelen, L.: An exercise in iterative domain-specific language design. In: EVOL\/IWPSE. pp. 48\u201357. ACM (2010)","DOI":"10.1145\/1862372.1862386"},{"key":"8_CR2","unstructured":"Baalen, J.V., Robinson, P., Lowry, M., Pressburger, T.: Explaining synthesized software. In: ASE. pp. 240\u2013248. IEEE (1998)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science (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. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)"},{"key":"8_CR4","unstructured":"Blech, J., Glesner, S., Leitner, J.: Formal verification of java code generation from UML models. In: Fujaba Days, pp. 49\u201356 (2005)"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/1047659.1040327","volume":"40","author":"R Bornat","year":"2005","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. ACM SIGPLAN Not. 40(1), 259\u2013270 (2005)","journal-title":"ACM SIGPLAN Not."},{"issue":"3","key":"8_CR6","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K., Poll, E.: An overview of JML tools and applications. STTT 7(3), 212\u2013232 (2005)","journal-title":"STTT"},{"key":"8_CR7","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":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T., Poll, E., Kiniry, J.R., Chalin, P.: Beyond assertions: advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Denney, E., Fischer, B.: Generating customized verifiers for automatically generated code. In: GPCE, pp. 77\u201388. ACM (2008)","DOI":"10.1145\/1449913.1449926"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Denney, E., Fischer, B., Schumann, J., Richardson, J.: Automatic certification of kalman filters for reliable code generation. In: IEEE Aerospace Conference. pp. 1\u201310. IEEE (2005)","DOI":"10.1109\/AERO.2005.1559605"},{"key":"8_CR11","series-title":"From Semaphores to Remote Procedure Calls","first-page":"65","volume-title":"The Origin of Concurrent Programming","author":"EW Dijkstra","year":"2002","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: Brinch Hansen, P. (ed.) The Origin of Concurrent Programming. From Semaphores to Remote Procedure Calls, pp. 65\u2013138. Springer, New York (2002)"},{"key":"8_CR12","unstructured":"Fogelberg, C., Potanin, A., Noble, J.: Ownership meets java. In: IWACO, pp. 30\u201333 (2007)"},{"issue":"10","key":"8_CR13","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"8_CR14","series-title":"From Semaphores to Remote Procedure Calls","first-page":"231","volume-title":"The Origin of Concurrent Programming","author":"CAR Hoare","year":"2002","unstructured":"Hoare, C.A.R.: Towards a Theory of Parallel Programming. In: Brinch Hansen, P. (ed.) The Origin of Concurrent Programming. From Semaphores to Remote Procedure Calls, pp. 231\u2013244. Springer, New York (2002)"},{"key":"8_CR15","unstructured":"Jacobs, B.: VeriFast website. people.cs.kuleuven.be\/ $$\\sim $$ bart.jacobs\/verifast\/ (2012)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: POPL, pp. 271\u2013282. ACM (2011)","DOI":"10.1145\/1925844.1926417"},{"issue":"4","key":"8_CR17","doi-asserted-by":"publisher","first-page":"21: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), 21:1\u201321:54 (2009)","journal-title":"ACM Comput. Surv."},{"key":"8_CR18","unstructured":"Kleppe, A., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture(TM): Practice and Promise. Addison-Wesley Professional, Boston (2005)"},{"issue":"1\u20132","key":"8_CR19","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The krakatoa tool for certification of java\/javacard programs annotated in JML. J. Logic Algebraic Program. 58(1\u20132), 89\u2013106 (2004)","journal-title":"J. Logic Algebraic Program."},{"key":"8_CR20","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":"PW O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"issue":"5","key":"8_CR21","doi-asserted-by":"publisher","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"},{"issue":"2","key":"8_CR22","doi-asserted-by":"publisher","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":"8_CR23","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"8_CR24","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., Reif, W., Moebius, N.: 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":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-39038-8_14","volume-title":"ECOOP 2013 \u2013 Object-Oriented Programming","author":"K Svendsen","year":"2013","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Joins: a case study in modular specification of a concurrent reentrant higher-order library. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 327\u2013351. Springer, Heidelberg (2013)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-37036-6_11","volume-title":"Programming Languages and Systems","author":"M Parkinson","year":"2013","unstructured":"Parkinson, M., Birkedal, L., Svendsen, K.: Modular reasoning about separation of concurrent data structures. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 169\u2013188. Springer, Heidelberg (2013)"},{"key":"8_CR27","unstructured":"Welch, P., Martin, J.: Formal analysis of concurrent java systems. In: CPA, pp. 275\u2013301. IOS Press (2000)"},{"key":"8_CR28","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":"8_CR29","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":"8_CR30","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":"L Engelen","year":"2014","unstructured":"Engelen, L., Wijs, A.: 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)"},{"key":"8_CR31","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":"8_CR32","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 (2014). CEUR-WS.org"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Zibin, Y., Potanin, A., Li, P., Ali, M., Ernst, M.: Ownership and immutability in generic java. In: OOPSLA. ACM SIGPLAN Notices, vol. 45, pp. 598\u2013617. ACM (2010)","DOI":"10.1145\/1932682.1869509"}],"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-319-28934-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T07:41:40Z","timestamp":1748763700000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-28934-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319289335","9783319289342"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-28934-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}