{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:24:33Z","timestamp":1759332273321,"version":"3.37.3"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T00:00:00Z","timestamp":1672963200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T00:00:00Z","timestamp":1672963200000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,2]]},"DOI":"10.1007\/s10009-022-00692-w","type":"journal-article","created":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T20:02:39Z","timestamp":1673035359000},"page":"77-94","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Go2Pins: a framework for the LTL verification of Go programs (extended version)"],"prefix":"10.1007","volume":"25","author":[{"given":"Alexandre","family":"Kirszenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3263-7669","authenticated-orcid":false,"given":"Antoine","family":"Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hugo","family":"Moreau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9013-4413","authenticated-orcid":false,"given":"Etienne","family":"Renault","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,1,6]]},"reference":[{"key":"692_CR1","unstructured":"Baranova, Z., Barnat, J., Kejstova, K., Kucera, T., Lauko, H., Mrazek, J., Rockai, P., Still, V.: Model checking of C and C++ with DIVINE 4. In ATVA\u201917, vol. 10482 of LNCS, pp. 201\u2013207. Springer, (2017)"},{"key":"692_CR2","doi-asserted-by":"crossref","unstructured":"Berthelot, G.: Checking properties of nets using transformation. In Applications and Theory in Petri Nets, vol. 222 of LNCS, pp. 19\u201340. Springer, (1985)","DOI":"10.1007\/BFb0016204"},{"key":"692_CR3","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Le\u00a0Botlan, D., Dal\u00a0Zilio, S.: Counting Petri net markings from reduction equations. Int. J. Softw. Tools Technol. Transf. (2019)","DOI":"10.1007\/s10009-019-00519-1"},{"key":"692_CR4","doi-asserted-by":"crossref","unstructured":"Blahoudek, F., Duret-Lutz, A., Rujbr, V., Strej\u010dek, J.: On refinement of B\u00fcchi automata for explicit model checking. In SPIN\u201915, vol. 9232 of LNCS, pp. 66\u201383. Springer, Aug. (2015)","DOI":"10.1007\/978-3-319-23404-5_6"},{"key":"692_CR5","doi-asserted-by":"crossref","unstructured":"Bloemen, V., van de Pol, J.: Multi-core scc-based ltl model checking. In HVC\u201916, vol. 10028 of LNCS, pp. 18\u201333. Springer, Nov. (2016)","DOI":"10.1007\/978-3-319-49052-6_2"},{"key":"692_CR6","unstructured":"Dekker, J., Vaandrager, F., Smetsers, R.: Generating a google go framework from an uppaal model. Master\u2019s thesis. Radboud University (2014)"},{"key":"692_CR7","doi-asserted-by":"crossref","unstructured":"Dilley, N., Lange, J.: An empirical study of messaging passing concurrency in go projects. In 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER\u201919), pp. 377\u2013387, (2019)","DOI":"10.1109\/SANER.2019.8668036"},{"key":"692_CR8","doi-asserted-by":"publisher","first-page":"34","DOI":"10.4204\/EPTCS.314.4","volume":"314","author":"N Dilley","year":"2020","unstructured":"Dilley, N., Lange, J.: Bounded verification of message-passing concurrency in go using promela and spin. Electr. Proc. Theor. Comput. Sci. 314, 34\u201345 (2020). https:\/\/doi.org\/10.4204\/EPTCS.314.4","journal-title":"Electr. Proc. Theor. Comput. Sci."},{"key":"692_CR9","doi-asserted-by":"crossref","unstructured":"Dilley,N., Lange, J.: Automated verification of go programs via bounded model checking. In 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 1016\u20131027, (2021)","DOI":"10.1109\/ASE51524.2021.9678571"},{"key":"692_CR10","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 \u2014 a framework for LTL and $$\\omega $$-automata manipulation. In ATVA\u201916, vol. 9938 of LNCS, pp. 122\u2013129. Springer, Oct. (2016)","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"692_CR11","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Series on Integrated Circuits and Systems (2006)"},{"key":"692_CR12","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Laarman, A., Petrucci, L., van\u00a0de Pol, J.: Improved multi-core nested depth-first search. In ATVA\u201912, vol. 7561 of LNCS, pp. 269\u2013283. Springer, (2012)","DOI":"10.1007\/978-3-642-33386-6_22"},{"key":"692_CR13","unstructured":"GitHub repository. Go Compiler. https:\/\/github.com\/golang\/go\/blob\/04fb929a5b7991ed0945d05ab8015c1721958d82\/src\/go\/types\/stmt.go#L67-L69"},{"key":"692_CR14","unstructured":"GitHub repository. Kubernetes generate node map bug. https:\/\/github.com\/kubernetes\/kubernetes\/blob\/d70ee902fddc682863a3cc4f0d8eac0223ebf70b\/test\/e2e\/storage\/vsphere\/nodemapper.godd#L62"},{"key":"692_CR15","unstructured":"GitHub repository. Trillian preload bug. https:\/\/github.com\/kubernetes\/kubernetes\/blob\/d70ee902fddc682863a3cc4f0d8eac0223ebf70b\/test\/e2e\/storage\/vsphere\/nodemapper.go#L62"},{"key":"692_CR16","unstructured":"GitHub repository. C2Go: Migrate from C to Go. https:\/\/godoc.org\/rsc.io\/c2go, (2020)"},{"key":"692_CR17","unstructured":"GitHub repository. C4Go: Transpiling C code to Go code. https:\/\/github.com\/Konstantin8105\/c4go, (2020)"},{"key":"692_CR18","unstructured":"GitHub repository. Transpiling fortran code to golang code. https:\/\/github.com\/Konstantin8105\/f4go, (2020)"},{"key":"692_CR19","unstructured":"GitHub repository. Grumpy: Go running Python. https:\/\/github.com\/google\/grumpy, (2020)"},{"key":"692_CR20","unstructured":"GitHub repository. Java2Go: Convert Java code to something like Go. https:\/\/github.com\/dglo\/java2go, (2020)"},{"key":"692_CR21","doi-asserted-by":"crossref","unstructured":"Giunti, M.: Gopi: Compiling linear and static channels in go. In Coordination Models and Languages, pp. 137\u2013152, (2020) Springer","DOI":"10.1007\/978-3-030-50029-0_9"},{"key":"692_CR22","unstructured":"Godefroid, P.: Between testing and verification: Dynamic software model checking. In DSSE\u201916 45, pp. 99\u2013116 (2016)"},{"key":"692_CR23","unstructured":"Griesemer,R., Pike, R., Thompson, K., Taylor, I., Cox, R., Kim, J., Langley, A.: Hey! ho! let\u2019s go! https:\/\/opensource.googleblog.com\/2009\/11\/hey-ho-lets-go.html, (2009)"},{"key":"692_CR24","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc, USA (1985)"},{"key":"692_CR25","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2003)"},{"key":"692_CR26","doi-asserted-by":"crossref","unstructured":"Kant, G., Laarman, A., Meijer, J., van\u00a0de Pol, J., Blom, S., van Dijk, T.: Ltsmin: high-performance language-independent model checking. In TACAS\u201915, pp. 692\u2013707, April (2015)","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"692_CR27","doi-asserted-by":"crossref","unstructured":"Kirszenberg,A., Martin, A., Moreau, H., Renault, E.: Go2Pins: a framework for the LTL verification of Go programs. In SPIN\u201921, vol. 12864 of LNCS, pp. 140\u2013156, May (2021) Springer","DOI":"10.1007\/978-3-030-84629-9_8"},{"key":"692_CR28","doi-asserted-by":"crossref","unstructured":"Laarman,A.: Stubborn transaction reduction. In NFM, vol. 10811 of LNCS, pp. 280\u2013298. Springer, (2018)","DOI":"10.1007\/978-3-319-77935-5_20"},{"key":"692_CR29","doi-asserted-by":"crossref","unstructured":"Laarman, A., Pater, E., van\u00a0de Pol, J.,\u00a0Hansen, H.: Guard-based partial-order reduction. Int. J. Softw. Tools Technol. Transf. 1\u201322, (2014)","DOI":"10.1007\/s10009-014-0363-9"},{"key":"692_CR30","doi-asserted-by":"crossref","unstructured":"Lange,J., Ng, N., Toninho, B., Yoshida, N.: Fencing off Go: Liveness and Safety for Channel-based Programming. In POPL\u201917, pp. 748\u2013761. ACM, (2017)","DOI":"10.1145\/3093333.3009847"},{"key":"692_CR31","doi-asserted-by":"crossref","unstructured":"Lange,J., Ng, N., Toninho, B., Yoshida, N.: A static verification framework for message passing in Go using behavioural Types. In CSE\u201918, pp. 1137\u20131148. ACM, (2018)","DOI":"10.1145\/3180155.3180157"},{"issue":"12","key":"692_CR32","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"692_CR33","unstructured":"Liu, Z., Zhu, S., Qin, B., Chen, H., Song, L.: Automatically detecting and fixing concurrency bugs in go software systems. In: International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) 11, pp. 2227\u20132240 (2016)"},{"key":"692_CR34","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In PODC\u201990, pp. 377\u2013410, (1990) ACM","DOI":"10.1145\/93385.93442"},{"key":"692_CR35","doi-asserted-by":"crossref","unstructured":"Ng, N., Yoshida, N.: Static deadlock detection for concurrent go by global session graph synthesis. In CCC\u201916, pp. 174\u2013184. ACM, (2016)","DOI":"10.1145\/2892208.2892232"},{"key":"692_CR36","doi-asserted-by":"crossref","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In CAV\u201994, vol. 818 of LNCS, pp. 377\u2013390. Springer, (1994)","DOI":"10.1007\/3-540-58179-0_69"},{"key":"692_CR37","doi-asserted-by":"crossref","unstructured":"Ray, B., Posnett, D., Filkov, V., Devanbu, P.: A large scale study of programming languages and code quality in github. In SIGSOFT\u201914, pp. 155\u2013165, (2014)","DOI":"10.1145\/2635868.2635922"},{"key":"692_CR38","unstructured":"RERS challenge. Rigorous examination of reactive systems (RERS). http:\/\/rers-challenge.org\/2019\/, (2019)"},{"key":"692_CR39","doi-asserted-by":"crossref","unstructured":"Tu, T., Liu, X., Song, L., Zhang, Y.: Understanding real-world concurrency bugs in go. In ASPLOS\u201919, pp. 865\u2013878, (2019)","DOI":"10.1145\/3297858.3304069"},{"key":"692_CR40","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In ICATPN\u201991, vol. 618 of LNCS, pp. 491\u2013515, (1991) Springer","DOI":"10.1007\/3-540-53863-1_36"},{"key":"692_CR41","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. In ASE\u201903 10, pp. 203\u2013232 (2018)","DOI":"10.1023\/A:1022920129859"},{"key":"692_CR42","doi-asserted-by":"crossref","unstructured":"Yuan, T., Li, G., Lu, J., Liu, C., Li, L., Xue, J.: Gobench: A benchmark suite of real-world go concurrency bugs. In 2021 IEEE\/ACM International Symposium on Code Generation and Optimization (CGO), pp. 187\u2013199, (2021)","DOI":"10.1109\/CGO51591.2021.9370317"},{"key":"692_CR43","unstructured":"Zaks, A., Joshi, R.: Verifying Multi-threaded C Programs with SPIN. In SPIN\u201908, pp. 94\u2013107, (2008)"},{"key":"692_CR44","unstructured":"Zhong,C., Zhao, Q., Liu, X.: Bingo: Pinpointing concurrency bugs in go via binary analysis, (2022)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00692-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00692-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00692-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T17:09:15Z","timestamp":1678295355000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00692-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,6]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,2]]}},"alternative-id":["692"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00692-w","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2023,1,6]]},"assertion":[{"value":"29 November 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 January 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}