{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T22:44:27Z","timestamp":1763765067045,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031765537"},{"type":"electronic","value":"9783031765544"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-76554-4_12","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T11:17:54Z","timestamp":1731410274000},"page":"217-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["VeyMont: Choreography-Based Generation of\u00a0Correct Concurrent Programs with\u00a0Shared Memory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5638-5945","authenticated-orcid":false,"given":"Robert","family":"Rubbens","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9212-1525","authenticated-orcid":false,"given":"Petra van den","family":"Bos","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4467-072X","authenticated-orcid":false,"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Armborst, L., et al.: The VerCors verifier: a progress report. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14682, pp. 3\u201318. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_1","DOI":"10.1007\/978-3-031-65630-9_1"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-662-46675-9_14","volume-title":"Fundamental Approaches to Software Engineering","author":"S Blom","year":"2015","unstructured":"Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 202\u2013217. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_14"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The vercors tool set: Verification of parallel and concurrent software. In: Lecture Notes in Computer Science, pp. 102\u2013110. Springer International Publishing (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"12_CR4","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364. Wroc\u0142aw, Poland, August 2011"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06269, pp. 162\u2013176. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pp. 259\u2013270. ACM (2005). https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"van\u00a0den Bos, P., Jongmans, S.: Veymont: Parallelising verified programs instead of verifying parallel programs. In: Chechik, M., Katoen, J., Leucker, M. (eds.) Formal Methods - 25th International Symposium, FM 2023, L\u00fcbeck, Germany, March 6-10, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14000, pp. 321\u2013339. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_19","DOI":"10.1007\/978-3-031-27481-7_19"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Bouma, J., de\u00a0Gouw, S., Jongmans, S.: Multiparty session typing in java, deductively. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II. LNCS, vol. 13994, pp. 19\u201327. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_3","DOI":"10.1007\/978-3-031-30820-8_3"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Carbone, M., Grohmann, D., Hildebrandt, T.T., L\u00f3pez, H.A.: A logic for choreographies. In: Honda, K., Mycroft, A. (eds.) Proceedings Third Workshop on Programming Language Approaches to Concurrency and communication-cEntric Software, PLACES 2010, Paphos, Cyprus, 21st March 2010. EPTCS, vol.\u00a069, pp. 29\u201343 (2010). https:\/\/doi.org\/10.4204\/EPTCS.69.3","DOI":"10.4204\/EPTCS.69.3"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Graversen, E., Montesi, F., Peressotti, M.: Reasoning about choreographic programs. In: Jongmans, S., Lopes, A. (eds.) Coordination Models and Languages - 25th IFIP WG 6.1 International Conference, COORDINATION 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13908, pp. 144\u2013162. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-35361-1_8","DOI":"10.1007\/978-3-031-35361-1_8"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Haack, C., Huisman, M., Hurlin, C.: Reasoning about java\u2019s reentrant locks. In: Ramalingam, G. (ed.) Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings. LNCS, vol.\u00a05356, pp. 171\u2013187. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-89330-1_13","DOI":"10.1007\/978-3-540-89330-1_13"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Hinrichsen, J.K., Bengtson, J., Krebbers, R.: Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang. 4(POPL), 6:1\u20136:30 (2020). https:\/\/doi.org\/10.1145\/3371074","DOI":"10.1145\/3371074"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) Programming Languages and Systems - ESOP\u201998, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201998, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings. Lecture Notes in Computer Science, vol.\u00a01381, pp. 122\u2013138. Springer (1998). https:\/\/doi.org\/10.1007\/BFB0053567","DOI":"10.1007\/BFB0053567"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Jacobs, J., Hinrichsen, J.K., Krebbers, R.: Dependent session protocols in separation logic from first principles (functional pearl). Proc. ACM Program. Lang. 7(ICFP), 768\u2013795 (2023). https:\/\/doi.org\/10.1145\/3607856","DOI":"10.1145\/3607856"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Jongmans, S., van\u00a0den Bos, P.: A predicate transformer for choreographies - computing preconditions in choreographic programming. In: Sergey, I. (ed.) Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13240, pp. 520\u2013547. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_19","DOI":"10.1007\/978-3-030-99336-8_19"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Marques, E.R.B., Martins, F., Vasconcelos, V.T., Ng, N., Martins, N.: Towards deductive verification of MPI programs against session types. In: Yoshida, N., Vanderbauwhede, W. (eds.) Proceedings 6th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2013, Rome, Italy, 23rd March 2013. EPTCS, vol.\u00a0137, pp. 103\u2013113 (2013). https:\/\/doi.org\/10.4204\/EPTCS.137.9","DOI":"10.4204\/EPTCS.137.9"},{"key":"12_CR17","unstructured":"Message Passing Interface Forum: MPI: A Message-Passing Interface Standard Version 4.0 June 2021. https:\/\/www.mpi-forum.org\/docs\/mpi-4.0\/mpi40-report.pdf"},{"key":"12_CR18","doi-asserted-by":"publisher","DOI":"10.1017\/9781108981491","author":"F Montesi","year":"2023","unstructured":"Montesi, F.: Introduction to Choreographies. Cambridge University Press (2023). https:\/\/doi.org\/10.1017\/9781108981491","journal-title":"Introduction to Choreographies. Cambridge University Press"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Neykova, R., Yoshida, N., Hu, R.: SPY: local verification of global protocols. In: Legay, A., Bensalem, S. (eds.) Runtime Verification - 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013. Proceedings. LNCS, vol.\u00a08174, pp. 358\u2013363. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_25","DOI":"10.1007\/978-3-642-40787-1_25"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Proust, O., Loulergue, F.: Verified scalable parallel computing with why3. In: Ferreira, C., Willemse, T.A.C. (eds.) Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14323, pp. 246\u2013262. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-47115-5_14","DOI":"10.1007\/978-3-031-47115-5_14"},{"key":"12_CR21","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.13348214","author":"R Rubbens","year":"2024","unstructured":"Rubbens, R., van den Bos, P., Huisman, M.: VeyMont permission annotations tic-tac-toe case studies and tool implementation (2024). https:\/\/doi.org\/10.5281\/zenodo.13348214","journal-title":"VeyMont permission annotations tic-tac-toe case studies and tool implementation"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Sakar, \u00d6., Safari, M., Huisman, M., Wijs, A.: Alpinist: An annotation-aware GPU program optimizer. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13244, pp. 332\u2013352. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_18","DOI":"10.1007\/978-3-030-99527-0_18"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Swamy, N., Hritcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P., Kohlweiss, M., Zinzindohoue, J.K., B\u00e9guelin, S.Z.: Dependent types and multi-monadic effects in F. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 256\u2013270. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837655","DOI":"10.1145\/2837614.2837655"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Swamy, N., Rastogi, A., Fromherz, A., Merigoux, D., Ahman, D., Mart\u00ednez, G.: Steelcore: an extensible concurrent separation logic for effectful dependently typed programs. Proc. ACM Program. Lang. 4(ICFP), 121:1\u2013121:30 (2020). https:\/\/doi.org\/10.1145\/3409003","DOI":"10.1145\/3409003"},{"key":"12_CR25","unstructured":"Vercors tool homepage. https:\/\/utwente.nl\/vercors. Accessed 01 Mar 2024"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Yoshida, N., Hu, R., Neykova, R., Ng, N.: The scribble protocol language. In: Abadi, M., Lluch-Lafuente, A. (eds.) Trustworthy Global Computing - 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers. LNCS, vol.\u00a08358, pp. 22\u201341. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-05119-2_3","DOI":"10.1007\/978-3-319-05119-2_3"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang. 4(OOPSLA), 148:1\u2013148:30 (2020). https:\/\/doi.org\/10.1145\/3428216","DOI":"10.1145\/3428216"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-76554-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T11:38:10Z","timestamp":1737200290000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-76554-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031765537","9783031765544"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-76554-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Manchester","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2024.cs.manchester.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}